Overlapping families (specificity/degrees of freedom)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Overlapping families (specificity/degrees of freedom)

Gabor Greif-2
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


Reply | Threaded
Open this post in threaded view
|

Overlapping families (specificity/degrees of freedom)

Richard Eisenberg-2
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



Reply | Threaded
Open this post in threaded view
|

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


Reply | Threaded
Open this post in threaded view
|

Overlapping families (specificity/degrees of freedom)

Gabor Greif-2
In reply to this post by Richard Eisenberg-2
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
>
>


Reply | Threaded
Open this post in threaded view
|

Overlapping families (specificity/degrees of freedom)

Gabor Greif-2
Errr. Messed this up, correction:

> minUnion :: DecEq a b -> Sing (a :: Symbol) -> Sing (b :: Symbol) -> Sing (MinUnion a b)
> minUnion (Right Refl) a b -> Cons a Nil
> minUnion (Left disproved) a b -> Cons a (Cons b Nil)

Anyway will GHC understand that a != b given (Left disproved) and thus
exclude the first case in MinUnion, which would in turn allow to
unambiguously select the second case of MinUnion?

Or is GHCs type-level logic still unprepared to see the (Inhabited ->
Uninhabited) type-level facts as negation?

    Gabor


Reply | Threaded
Open this post in threaded view
|

Overlapping families (specificity/degrees of freedom)

Richard Eisenberg-2
In reply to this post by Gabor Greif-2

On Apr 3, 2013, at 3:01 PM, Gabor Greif <ggreif at gmail.com> wrote:

>
> 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
> }}}
>

I think you're out of luck with this approach, I'm afraid. GHC does not know how to use something like (a :~: b -> Void) as evidence of inequality -- not by a long shot. The best thing I can think of is to use a "normal" promoted data type instead of Symbol, so you can write a recursive equality function and avoid "type instance where". I think, then, you'd be able to get it all to work out. "type instance where" and GADT pattern matching don't really play nicely with each other.

>
>>
>>> {-# 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?

Well, sort of. I cheat a little. `Eq` is not promoted to the type level, but that's OK. There is a type family (:==:) that 'singletons' has for type-level Boolean equality. That type family only has instances for datatypes that have Eq instances, at the value level. There is no real need to promote the constraint. `member` and `intersect` are promoted to the type level to become `Member` and `Intersect`. They are also refined into functions that process singletons, called `sMember` and `sIntersect`. Equality is refined into a function over singletons called `%==%`, and the type class for singleton types with equality is called `SEq`.

One problem with all of this is that it doesn't really work with Symbols, because Symbols aren't recursively defined. Using unsafe features, we can squeeze out an instance of `SEq` (which would, in fact, be safe, but GHC wouldn't know it), but without inequality evidence, I don't think there's a way to get a branched type family instance (a "type instance where") to do the right thing. Somehow, to get that instance to trigger, you need to show GHC that the two types have different constructors used somewhere in their structure. Because Symbols have no structure, this isn't possible.

Richard