On 3/14/13, Richard Eisenberg <e...@cis.upenn.edu> wrote: > 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 > > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
