Richard (or anyone else) Now that you have taken the time to type this in, I wonder if some of it might usefully be in the user manual and/or the Haskell Wiki user-facing supplementary documentation ? Seems a shame to waste it! Simon | -----Original Message----- | From: ghc-devs-bounces@haskell.org [mailto:ghc-devs-bounces@haskell.org] On | Behalf Of Richard Eisenberg | Sent: 14 March 2013 17:42 | To: Gabor Greif | Cc: ghc-devs | Subject: Re: Overlapping families (specificity/degrees of freedom) | | 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. | | 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. | | I hope this helps you understand why your code isn't working. | | 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: | | > {-# 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 | > |]) | | 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? | | 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