On Apr 3, 2013, at 3:01 PM, Gabor Greif <ggr...@gmail.com> wrote:
>
> What I want is a function that can e.g. create the minimal union of
> two Symbol singletons, possibly by consulting decidable (in)equality:
>
> {{{ (sketch)
> type family MinUnion (a :: Symbol) (b :: Symbol) :: [Symbol]
> type instance where
> MinUnion a a = '[a]
> MinUnion a b = '[a, b]
>
> minUnion :: DecEq a b -> Sing (a :: Symbol) -> Sing (b :: Symbol) ->
> Sing (MinUnion a b)
> minUnion (Right Refl) a b -> Cons a Nil
> minUnion (Left Refl) a b -> Cons a b
> }}}
>
I think you're out of luck with this approach, I'm afraid. GHC does not know
how to use something like (a :~: b -> Void) as evidence of inequality -- not by
a long shot. The best thing I can think of is to use a "normal" promoted data
type instead of Symbol, so you can write a recursive equality function and
avoid "type instance where". I think, then, you'd be able to get it all to work
out. "type instance where" and GADT pattern matching don't really play nicely
with each other.
>
>>
>>> {-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, TypeFamilies, GADTs,
>>> UndecidableInstances, FlexibleContexts, RankNTypes #-}
>>>
>>> import Data.Singletons
>>>
>>> $(singletons [d|
>>> member :: Eq a => a -> [a] -> Bool
>>> member _ [] = False
>>> member x (h : t) = x == h || member x t
>>>
>>> intersect :: Eq a => [a] -> [a] -> [a]
>>> intersect [] _ = []
>>> intersect (h : t) b = if member h b then h : (intersect t b) else
>>> intersect t b
>>> |])
>
> You appear to be able to lift `Eq a` up to the type level (and
> `member` too) as a type function. How do you compare Symbol? Also,will
> this give me an `intersect` function at the value level?
Well, sort of. I cheat a little. `Eq` is not promoted to the type level, but
that's OK. There is a type family (:==:) that 'singletons' has for type-level
Boolean equality. That type family only has instances for datatypes that have
Eq instances, at the value level. There is no real need to promote the
constraint. `member` and `intersect` are promoted to the type level to become
`Member` and `Intersect`. They are also refined into functions that process
singletons, called `sMember` and `sIntersect`. Equality is refined into a
function over singletons called `%==%`, and the type class for singleton types
with equality is called `SEq`.
One problem with all of this is that it doesn't really work with Symbols,
because Symbols aren't recursively defined. Using unsafe features, we can
squeeze out an instance of `SEq` (which would, in fact, be safe, but GHC
wouldn't know it), but without inequality evidence, I don't think there's a way
to get a branched type family instance (a "type instance where") to do the
right thing. Somehow, to get that instance to trigger, you need to show GHC
that the two types have different constructors used somewhere in their
structure. Because Symbols have no structure, this isn't possible.
Richard
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
