Overlapping families (specificity/degrees of freedom)

[Simon Peyton-Jones]

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 at haskell.org [mailto:ghc-devs-bounces at 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 at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs