Overlapping families (specificity/degrees of freedom)
Simon PeytonJones
simonpj at microsoft.com
Fri Mar 15 09:30:25 CET 2013
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 userfacing supplementary documentation
?
Seems a shame to waste it!
Simon
 Original Message
 From: ghcdevsbounces at haskell.org [mailto:ghcdevsbounces at haskell.org] On
 Behalf Of Richard Eisenberg
 Sent: 14 March 2013 17:42
 To: Gabor Greif
 Cc: ghcdevs
 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 lefthand 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 lefthand
 side of the branch coincide with the (substituted) type family application.

 Another way to state (2) is that the lefthand 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 termlevel 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 nonequality witness to trigger the fourth leg
 > of InterAppend above?
 >
 > What I am trying to implement is an intersection algorithm for
 > singletontyped 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


 _______________________________________________
 ghcdevs mailing list
 ghcdevs at haskell.org
 http://www.haskell.org/mailman/listinfo/ghcdevs
More information about the ghcdevs
mailing list