On 3/14/13, Richard Eisenberg
Hi Gabor,
I can't comment specifically on your code, because I'm afraid I don't understand it all. But, I think I can answer your question:
GHC will select a type instance branch to use in a given type family application if and only if the following 2 conditions hold: 1. There is a substitution from the variables in the branch statement that makes the left-hand side of the branch coincide with the type family application. 2. There exists *no* substitution from the variables in the branch statement ***and the variables in the type family application*** that make the left-hand side of the branch coincide with the (substituted) type family application.
Another way to state (2) is that the left-hand side of the branch must not *unify* with the type family application. In your example, this means that GHC must be sure that 'r' and 'one' are distinct types before selecting the fourth branch.
Why do this? It's a matter of type safety. Say GHC selected the fourth branch just because the third one doesn't apply at the moment, because the type variables in the application are distinct. The problem is that those variables might later be instantiated at the same value, and then the third branch would have applied. You can convince this sort of inconsistency to produce unsafeCoerce.
Yep.
It gets worse. GHC has no internal notion of inequality, so it can't use previous, failed term-level GADT pattern matches to refine its type assumptions. For example:
data G :: * -> * where GInt :: G Int GBool :: G Bool
type family Foo (a :: *) :: * type instance where Foo Int = Char Foo a = Double
bar :: G a -> Foo a bar GInt = 'x' bar _ = 3.14
The last line will fail to typecheck, because GHC doesn't know that the type variable 'a' can't be Int here, even though it's obvious. The only general way I can see to fix this is to have inequality evidence introduced into GHC, and that's a big deal and I don't know if we have the motivation for such a change yet.
Right. Same for Omega. I have even written an issue for post-facto type inference years ago ( https://code.google.com/p/omega/issues/detail?id=12 :-)
I hope this helps you understand why your code isn't working.
Sure thing. 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 }}}
On the other hand, have you looked at the singletons library I wrote last year? The library takes normal code and, using Template Haskell, "singletonizes" it. For example:
No, I did not install singletons yet, too many other things around. But I have a question below...
{-# 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?
This works on GHC 7.6.1 and HEAD. Does it do what you want?
Richard
PS: You said Omega has a different policy about type family reduction. How does that deal with the problem I've discussed here?
Let's put this question on hold, I'll definitively come back with an answer later. Cheers, Gabor
On Mar 14, 2013, at 12:35 PM, Gabor Greif wrote:
Hi Richard,
I have a question regarding type families with overlapping syntax.
In below example the last two lines are overlapped, so the first gets selected when I present type equality witness to GHC:
help :: Sing (ls :: Inventory a) -> Sing (r :: Inventory a) -> Sing (l :: a) -> Sing (InterAppend ls r l) help l@(Snoc _ _) (Snoc _ r) one | Just Eq <- isSame r one = Snoc l one --- OKAY
type family InterAppend (l' :: Inventory a) (r' :: Inventory a) (one' :: a) :: Inventory a type instance where InterAppend Empty r one = Empty InterAppend (More ls l) Empty one = Empty InterAppend (More ls l) (More rs one) one = More (More ls l) one --- 4 degrees of freedom InterAppend (More ls l) (More rs r) one = More ls l --- 5 degrees of freedom
However I cannot manage to trigger the last line when *not* presenting the witness, e.g. in this case:
help l@(Snoc _ _) (Snoc _ _) _ = l --- DOES NOT WORK
IIRC, when implementing something like this in Omega, the type function evaluator considered the number of type variables and tried to match the more constrained leg (i.e. preferred less degrees of freedom).
Can you give me a hint how this is supposed to work in your implementation?
Must I present a type non-equality witness to trigger the fourth leg of InterAppend above?
What I am trying to implement is an intersection algorithm for singleton-typed list witnesses, roughly
intersect :: SingEqual (t :: a) => Sing (lhs :: '[a]) -> Sing (rhs :: '[a]) -> Sing (Intersect lhs rhs)
... but I am not there yet, obviously!
I'd be grateful for any hint,
cheers,
Gabor