Overlapping families (specificity/degrees of freedom)

[Gabor Greif]

On 3/14/13, Richard Eisenberg <eir at 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
>
>