Trouble with injective type families

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

Trouble with injective type families

Wolfgang Jeltsch-3
Hi!

Injective type families as supported by GHC 8.0.1 do not behave like I
would expect them to behave from my intuitive understanding.

Let us consider the following example:

> {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
>
> class C a where
>
>     type T a = b | b -> a
>
> instance C Bool where
>
>     type T Bool = Int
>
> type X b = forall a . T a ~ b => a
>
> x :: X Int
> x = False

I would expect this code to be accepted. However, I get the following
error message:

> A.hs:14:5: error:
>     • Could not deduce: a ~ Bool
>       from the context: T a ~ Int
>         bound by the type signature for:
>                    x :: T a ~ Int => a
>         at A.hs:13:1-10
>       ‘a’ is a rigid type variable bound by
>         the type signature for:
>           x :: forall a. T a ~ Int => a
>         at A.hs:11:19
>     • In the expression: False
>       In an equation for ‘x’: x = False
>     • Relevant bindings include x :: a (bound at A.hs:14:1)

This is strange, since injectivity should exactly make it possible to
deduce a ~ Bool from T a ~ Int.

Another example is this:

> {-# LANGUAGE GADTs, TypeFamilyDependencies #-}
>
> class C a where
>
>     type T a = b | b -> a
>
> instance C Bool where
>
>     type T Bool = Int
>
> data G b where
>
>     G :: Eq a => a -> G (T a)
>
> instance Eq (G b) where
>
>     G a1 == G a2 = a1 == a2a

I would also expect this code to be accepted. However, I get the
following error message:

> B.hs:17:26: error:
>     • Could not deduce: a1 ~ a
>       from the context: (b ~ T a, Eq a)
>         bound by a pattern with constructor:
>                    G :: forall a. Eq a => a -> G (T a),
>                  in an equation for ‘==’
>         at B.hs:17:5-8
>       or from: (b ~ T a1, Eq a1)
>         bound by a pattern with constructor:
>                    G :: forall a. Eq a => a -> G (T a),
>                  in an equation for ‘==’
>         at B.hs:17:13-16
>       ‘a1’ is a rigid type variable bound by
>         a pattern with constructor: G :: forall a. Eq a => a -> G (T a),
>         in an equation for ‘==’
>         at B.hs:17:13
>       ‘a’ is a rigid type variable bound by
>         a pattern with constructor: G :: forall a. Eq a => a -> G (T a),
>         in an equation for ‘==’
>         at B.hs:17:5
>     • In the second argument of ‘(==)’, namely ‘a2’
>       In the expression: a1 == a2
>       In an equation for ‘==’: (G a1) == (G a2) = a1 == a2
>     • Relevant bindings include
>         a2 :: a1 (bound at B.hs:17:15)
>         a1 :: a (bound at B.hs:17:7)

If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1,
because of injectivity. Unfortunately, GHC does not join the two
contexts (b ~ T a, Eq a) and (b ~ T a1, Eq a1).

Are these behaviors really intended, or are these bugs showing up?

All the best,
Wolfgang
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: Trouble with injective type families

Haskell - Glasgow-haskell-users mailing list
Functional dependencies and type-family dependencies only induce extra "improvement" constraints, not evidence.  For example

        class C a b | a -> b where foo :: a -> b
        instance C Bool Int where ...

        f :: C Bool b => b -> Int
        f x = x -- Rejected

Does the fundep on 'b' allow us to deduce (b ~ Int), GADT-like, in the body of 'f', and hence accept the definition.  No, it does not.  Think of the translation into System F. We get

        f = /\b \(d :: C Bool b). \(x::b).  x |> ???

What evidence can I used to cast 'x' by to get it from type 'b' to Int?

Rather, fundeps resolve ambiguity.  Consider

        g x = foo True + x

The call to 'foo True' gives rise to a "wanted" constraint (C Bool beta), where beta is a fresh unification variable.  Then by the fundep we get an "improvement" constraint (also "wanted") (beta ~ Int). So we can infer g :: Int -> Int.


In your example we have

   x :: forall a b. (T Int ~ b) => a
   x = False

Think of the System F translation:

   x = /\a b. \(d :: T Int ~ b). False |> ??

Again, what evidence can we use to cast False to 'a'.


In short, fundeps and type family dependencies only add extra unification constraints, which may help to resolve ambiguous types.  They don’t provide evidence.  That's not to say that they couldn't.  But you'd need to extend System FC, GHC's core language, to do so.

Simon


| -----Original Message-----
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| [hidden email]] On Behalf Of Wolfgang Jeltsch
| Sent: 05 July 2017 01:21
| To: [hidden email]
| Subject: Trouble with injective type families
|
| Hi!
|
| Injective type families as supported by GHC 8.0.1 do not behave like I
| would expect them to behave from my intuitive understanding.
|
| Let us consider the following example:
|
| > {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
| >
| > class C a where
| >
| >     type T a = b | b -> a
| >
| > instance C Bool where
| >
| >     type T Bool = Int
| >
| > type X b = forall a . T a ~ b => a
| >
| > x :: X Int
| > x = False
|
| I would expect this code to be accepted. However, I get the following
| error message:
|
| > A.hs:14:5: error:
| >     • Could not deduce: a ~ Bool
| >       from the context: T a ~ Int
| >         bound by the type signature for:
| >                    x :: T a ~ Int => a
| >         at A.hs:13:1-10
| >       ‘a’ is a rigid type variable bound by
| >         the type signature for:
| >           x :: forall a. T a ~ Int => a
| >         at A.hs:11:19
| >     • In the expression: False
| >       In an equation for ‘x’: x = False
| >     • Relevant bindings include x :: a (bound at A.hs:14:1)
|
| This is strange, since injectivity should exactly make it possible to
| deduce a ~ Bool from T a ~ Int.
|
| Another example is this:
|
| > {-# LANGUAGE GADTs, TypeFamilyDependencies #-}
| >
| > class C a where
| >
| >     type T a = b | b -> a
| >
| > instance C Bool where
| >
| >     type T Bool = Int
| >
| > data G b where
| >
| >     G :: Eq a => a -> G (T a)
| >
| > instance Eq (G b) where
| >
| >     G a1 == G a2 = a1 == a2a
|
| I would also expect this code to be accepted. However, I get the
| following error message:
|
| > B.hs:17:26: error:
| >     • Could not deduce: a1 ~ a
| >       from the context: (b ~ T a, Eq a)
| >         bound by a pattern with constructor:
| >                    G :: forall a. Eq a => a -> G (T a),
| >                  in an equation for ‘==’
| >         at B.hs:17:5-8
| >       or from: (b ~ T a1, Eq a1)
| >         bound by a pattern with constructor:
| >                    G :: forall a. Eq a => a -> G (T a),
| >                  in an equation for ‘==’
| >         at B.hs:17:13-16
| >       ‘a1’ is a rigid type variable bound by
| >         a pattern with constructor: G :: forall a. Eq a => a -> G (T
| > a),
| >         in an equation for ‘==’
| >         at B.hs:17:13
| >       ‘a’ is a rigid type variable bound by
| >         a pattern with constructor: G :: forall a. Eq a => a -> G (T
| > a),
| >         in an equation for ‘==’
| >         at B.hs:17:5
| >     • In the second argument of ‘(==)’, namely ‘a2’
| >       In the expression: a1 == a2
| >       In an equation for ‘==’: (G a1) == (G a2) = a1 == a2
| >     • Relevant bindings include
| >         a2 :: a1 (bound at B.hs:17:15)
| >         a1 :: a (bound at B.hs:17:7)
|
| If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1, because
| of injectivity. Unfortunately, GHC does not join the two contexts (b ~ T
| a, Eq a) and (b ~ T a1, Eq a1).
|
| Are these behaviors really intended, or are these bugs showing up?
|
| All the best,
| Wolfgang
| _______________________________________________
| Glasgow-haskell-users mailing list
| [hidden email]
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
| ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-
| users&data=02%7C01%7Csimonpj%40microsoft.com%7Cc333fbaff2f4406c337e08d4c3
| 3bd1bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636348109082017989&sd
| ata=q%2B8ZSqYfNjC7x6%2Bm9vpsgCmCDo%2FIItppqB5Nwzf6Qj0%3D&reserved=0
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Trouble with injective type families

Wolfgang Jeltsch-3
Dear Simon,

thank you very much for this elaborate explanation.

I stumbled on this issue when using functional dependencies years ago.
The solution at that time was to use type families.

I did not know that injectivity is handled analogously to functional
dependencies. Given that it is, the syntax for injectivity makes a lot
more sense.

All the best,
Wolfgang

Am Mittwoch, den 05.07.2017, 06:45 +0000 schrieb Simon Peyton Jones:

> Functional dependencies and type-family dependencies only induce extra
> "improvement" constraints, not evidence.  For example
>
> class C a b | a -> b where foo :: a -> b
> instance C Bool Int where ...
>
> f :: C Bool b => b -> Int
> f x = x -- Rejected
>
> Does the fundep on 'b' allow us to deduce (b ~ Int), GADT-like, in the
> body of 'f', and hence accept the definition.  No, it does not.  Think
> of the translation into System F. We get
>
> f = /\b \(d :: C Bool b). \(x::b).  x |> ???
>
> What evidence can I used to cast 'x' by to get it from type 'b' to
> Int?
>
> Rather, fundeps resolve ambiguity.  Consider
>
> g x = foo True + x
>
> The call to 'foo True' gives rise to a "wanted" constraint (C Bool
> beta), where beta is a fresh unification variable.  Then by the fundep
> we get an "improvement" constraint (also "wanted") (beta ~ Int). So we
> can infer g :: Int -> Int.
>
>
> In your example we have
>
>    x :: forall a b. (T Int ~ b) => a
>    x = False
>
> Think of the System F translation:
>
>    x = /\a b. \(d :: T Int ~ b). False |> ??
>
> Again, what evidence can we use to cast False to 'a'.
>
>
> In short, fundeps and type family dependencies only add extra
> unification constraints, which may help to resolve ambiguous
> types.  They don’t provide evidence.  That's not to say that they
> couldn't.  But you'd need to extend System FC, GHC's core language, to
> do so.
>
> Simon
>
>
> >
> > -----Original Message-----
> > From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
> > [hidden email]] On Behalf Of Wolfgang Jeltsch
> > Sent: 05 July 2017 01:21
> > To: [hidden email]
> > Subject: Trouble with injective type families
> >
> > Hi!
> >
> > Injective type families as supported by GHC 8.0.1 do not behave like
> > I
> > would expect them to behave from my intuitive understanding.
> >
> > Let us consider the following example:
> >
> > >
> > > {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
> > >
> > > class C a where
> > >
> > >     type T a = b | b -> a
> > >
> > > instance C Bool where
> > >
> > >     type T Bool = Int
> > >
> > > type X b = forall a . T a ~ b => a
> > >
> > > x :: X Int
> > > x = False
> > I would expect this code to be accepted. However, I get the
> > following
> > error message:
> >
> > >
> > > A.hs:14:5: error:
> > >     • Could not deduce: a ~ Bool
> > >       from the context: T a ~ Int
> > >         bound by the type signature for:
> > >                    x :: T a ~ Int => a
> > >         at A.hs:13:1-10
> > >       ‘a’ is a rigid type variable bound by
> > >         the type signature for:
> > >           x :: forall a. T a ~ Int => a
> > >         at A.hs:11:19
> > >     • In the expression: False
> > >       In an equation for ‘x’: x = False
> > >     • Relevant bindings include x :: a (bound at A.hs:14:1)
> > This is strange, since injectivity should exactly make it possible
> > to
> > deduce a ~ Bool from T a ~ Int.
> >
> > Another example is this:
> >
> > >
> > > {-# LANGUAGE GADTs, TypeFamilyDependencies #-}
> > >
> > > class C a where
> > >
> > >     type T a = b | b -> a
> > >
> > > instance C Bool where
> > >
> > >     type T Bool = Int
> > >
> > > data G b where
> > >
> > >     G :: Eq a => a -> G (T a)
> > >
> > > instance Eq (G b) where
> > >
> > >     G a1 == G a2 = a1 == a2a
> > I would also expect this code to be accepted. However, I get the
> > following error message:
> >
> > >
> > > B.hs:17:26: error:
> > >     • Could not deduce: a1 ~ a
> > >       from the context: (b ~ T a, Eq a)
> > >         bound by a pattern with constructor:
> > >                    G :: forall a. Eq a => a -> G (T a),
> > >                  in an equation for ‘==’
> > >         at B.hs:17:5-8
> > >       or from: (b ~ T a1, Eq a1)
> > >         bound by a pattern with constructor:
> > >                    G :: forall a. Eq a => a -> G (T a),
> > >                  in an equation for ‘==’
> > >         at B.hs:17:13-16
> > >       ‘a1’ is a rigid type variable bound by
> > >         a pattern with constructor: G :: forall a. Eq a => a -> G
> > > (T
> > > a),
> > >         in an equation for ‘==’
> > >         at B.hs:17:13
> > >       ‘a’ is a rigid type variable bound by
> > >         a pattern with constructor: G :: forall a. Eq a => a -> G
> > > (T
> > > a),
> > >         in an equation for ‘==’
> > >         at B.hs:17:5
> > >     • In the second argument of ‘(==)’, namely ‘a2’
> > >       In the expression: a1 == a2
> > >       In an equation for ‘==’: (G a1) == (G a2) = a1 == a2
> > >     • Relevant bindings include
> > >         a2 :: a1 (bound at B.hs:17:15)
> > >         a1 :: a (bound at B.hs:17:7)
> > If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1,
> > because
> > of injectivity. Unfortunately, GHC does not join the two contexts (b
> > ~ T
> > a, Eq a) and (b ~ T a1, Eq a1).
> >
> > Are these behaviors really intended, or are these bugs showing up?
> >
> > All the best,
> > Wolfgang
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > [hidden email]
> > https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail
> > .hask
> > ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-
> > users&data=02%7C01%7Csimonpj%40microsoft.com%7Cc333fbaff2f4406c337e0
> > 8d4c3
> > 3bd1bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6363481090820179
> > 89&sd
> > ata=q%2B8ZSqYfNjC7x6%2Bm9vpsgCmCDo%2FIItppqB5Nwzf6Qj0%3D&reserved=0
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Trouble with injective type families

Richard Eisenberg-4
I'd like to add that the reason we never extended System FC with support for injectivity is that the proof of soundness of doing so has remained elusive. A similar unsoundness in type improvement may cause unpredictable behavior in type inference, but it can't ever launch the rockets. So we keep it in type inference but out of FC.

Richard

> On Jul 5, 2017, at 9:37 AM, Wolfgang Jeltsch <[hidden email]> wrote:
>
> Dear Simon,
>
> thank you very much for this elaborate explanation.
>
> I stumbled on this issue when using functional dependencies years ago.
> The solution at that time was to use type families.
>
> I did not know that injectivity is handled analogously to functional
> dependencies. Given that it is, the syntax for injectivity makes a lot
> more sense.
>
> All the best,
> Wolfgang
>
> Am Mittwoch, den 05.07.2017, 06:45 +0000 schrieb Simon Peyton Jones:
>> Functional dependencies and type-family dependencies only induce extra
>> "improvement" constraints, not evidence.  For example
>>
>> class C a b | a -> b where foo :: a -> b
>> instance C Bool Int where ...
>>
>> f :: C Bool b => b -> Int
>> f x = x -- Rejected
>>
>> Does the fundep on 'b' allow us to deduce (b ~ Int), GADT-like, in the
>> body of 'f', and hence accept the definition.  No, it does not.  Think
>> of the translation into System F. We get
>>
>> f = /\b \(d :: C Bool b). \(x::b).  x |> ???
>>
>> What evidence can I used to cast 'x' by to get it from type 'b' to
>> Int?
>>
>> Rather, fundeps resolve ambiguity.  Consider
>>
>> g x = foo True + x
>>
>> The call to 'foo True' gives rise to a "wanted" constraint (C Bool
>> beta), where beta is a fresh unification variable.  Then by the fundep
>> we get an "improvement" constraint (also "wanted") (beta ~ Int). So we
>> can infer g :: Int -> Int.
>>
>>
>> In your example we have
>>
>>    x :: forall a b. (T Int ~ b) => a
>>    x = False
>>
>> Think of the System F translation:
>>
>>    x = /\a b. \(d :: T Int ~ b). False |> ??
>>
>> Again, what evidence can we use to cast False to 'a'.
>>
>>
>> In short, fundeps and type family dependencies only add extra
>> unification constraints, which may help to resolve ambiguous
>> types.  They don’t provide evidence.  That's not to say that they
>> couldn't.  But you'd need to extend System FC, GHC's core language, to
>> do so.
>>
>> Simon
>>
>>
>>>
>>> -----Original Message-----
>>> From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
>>> [hidden email]] On Behalf Of Wolfgang Jeltsch
>>> Sent: 05 July 2017 01:21
>>> To: [hidden email]
>>> Subject: Trouble with injective type families
>>>
>>> Hi!
>>>
>>> Injective type families as supported by GHC 8.0.1 do not behave like
>>> I
>>> would expect them to behave from my intuitive understanding.
>>>
>>> Let us consider the following example:
>>>
>>>>
>>>> {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
>>>>
>>>> class C a where
>>>>
>>>>     type T a = b | b -> a
>>>>
>>>> instance C Bool where
>>>>
>>>>     type T Bool = Int
>>>>
>>>> type X b = forall a . T a ~ b => a
>>>>
>>>> x :: X Int
>>>> x = False
>>> I would expect this code to be accepted. However, I get the
>>> following
>>> error message:
>>>
>>>>
>>>> A.hs:14:5: error:
>>>>     • Could not deduce: a ~ Bool
>>>>       from the context: T a ~ Int
>>>>         bound by the type signature for:
>>>>                    x :: T a ~ Int => a
>>>>         at A.hs:13:1-10
>>>>       ‘a’ is a rigid type variable bound by
>>>>         the type signature for:
>>>>           x :: forall a. T a ~ Int => a
>>>>         at A.hs:11:19
>>>>     • In the expression: False
>>>>       In an equation for ‘x’: x = False
>>>>     • Relevant bindings include x :: a (bound at A.hs:14:1)
>>> This is strange, since injectivity should exactly make it possible
>>> to
>>> deduce a ~ Bool from T a ~ Int.
>>>
>>> Another example is this:
>>>
>>>>
>>>> {-# LANGUAGE GADTs, TypeFamilyDependencies #-}
>>>>
>>>> class C a where
>>>>
>>>>     type T a = b | b -> a
>>>>
>>>> instance C Bool where
>>>>
>>>>     type T Bool = Int
>>>>
>>>> data G b where
>>>>
>>>>     G :: Eq a => a -> G (T a)
>>>>
>>>> instance Eq (G b) where
>>>>
>>>>     G a1 == G a2 = a1 == a2a
>>> I would also expect this code to be accepted. However, I get the
>>> following error message:
>>>
>>>>
>>>> B.hs:17:26: error:
>>>>     • Could not deduce: a1 ~ a
>>>>       from the context: (b ~ T a, Eq a)
>>>>         bound by a pattern with constructor:
>>>>                    G :: forall a. Eq a => a -> G (T a),
>>>>                  in an equation for ‘==’
>>>>         at B.hs:17:5-8
>>>>       or from: (b ~ T a1, Eq a1)
>>>>         bound by a pattern with constructor:
>>>>                    G :: forall a. Eq a => a -> G (T a),
>>>>                  in an equation for ‘==’
>>>>         at B.hs:17:13-16
>>>>       ‘a1’ is a rigid type variable bound by
>>>>         a pattern with constructor: G :: forall a. Eq a => a -> G
>>>> (T
>>>> a),
>>>>         in an equation for ‘==’
>>>>         at B.hs:17:13
>>>>       ‘a’ is a rigid type variable bound by
>>>>         a pattern with constructor: G :: forall a. Eq a => a -> G
>>>> (T
>>>> a),
>>>>         in an equation for ‘==’
>>>>         at B.hs:17:5
>>>>     • In the second argument of ‘(==)’, namely ‘a2’
>>>>       In the expression: a1 == a2
>>>>       In an equation for ‘==’: (G a1) == (G a2) = a1 == a2
>>>>     • Relevant bindings include
>>>>         a2 :: a1 (bound at B.hs:17:15)
>>>>         a1 :: a (bound at B.hs:17:7)
>>> If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1,
>>> because
>>> of injectivity. Unfortunately, GHC does not join the two contexts (b
>>> ~ T
>>> a, Eq a) and (b ~ T a1, Eq a1).
>>>
>>> Are these behaviors really intended, or are these bugs showing up?
>>>
>>> All the best,
>>> Wolfgang
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> [hidden email]
>>> https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail
>>> .hask
>>> ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-
>>> users&data=02%7C01%7Csimonpj%40microsoft.com%7Cc333fbaff2f4406c337e0
>>> 8d4c3
>>> 3bd1bd%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6363481090820179
>>> 89&sd
>>> ata=q%2B8ZSqYfNjC7x6%2Bm9vpsgCmCDo%2FIItppqB5Nwzf6Qj0%3D&reserved=0
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Trouble with injective type families

AntC
In reply to this post by Wolfgang Jeltsch-3
> On Wed Jul 5 14:16:10 UTC 2017, Richard Eisenberg wrote:

> I'd like to add that the reason we never extended System
FC
> with support for injectivity is that the proof of
soundness
> of doing so has remained elusive.

Thank you Richard, Simon.

IIRC the original FDs through CHRs paper did think it sound
to allow given `C a b1` and `C a b2` conclude `b1 ~ b2`
under a FunDep `a -> b`.
(I think that was also the case in Mark Jones'
 original paper on FunDeps.)

(See Iavor's comments on Trac #10675, for example.)

I know GHC's current FunDep inference is lax,
because there's good reasons to want 'wiggle room'
with FunDep (in)consistency.

I'm suggesting we could tighten that consistency check;
then we might make make FD inference stronger(?)
https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-312974557


AntC

>> Am Mittwoch, den 05.07.2017, 06:45 +0000 schrieb Simon
Peyton Jones:
>> Functional dependencies and type-family dependencies only
induce extra
>> "improvement" constraints, not evidence.  For example
>>
>> class C a b | a -> b where foo :: a -> b
>> instance C Bool Int where ...
>>
>> f :: C Bool b => b -> Int
>> f x = x -- Rejected
>>
>> Does the fundep on 'b' allow us to deduce (b ~ Int),
GADT-like, in the
>> body of 'f', and hence accept the definition.  No, it
does not.  Think

>> of the translation into System F. We get
>>
>> f = /\b \(d :: C Bool b). \(x::b).  x |> ???
>>
>> What evidence can I used to cast 'x' by to get it
>> from type 'b' to Int?
>>
>> Rather, fundeps resolve ambiguity.  Consider
>>
>> g x = foo True + x
>>
>> The call to 'foo True' gives rise to a "wanted"
constraint (C Bool
>> beta), where beta is a fresh unification variable.  Then
by the fundep
>> we get an "improvement" constraint (also "wanted") (beta
~ Int). So we

>> can infer g :: Int -> Int.
>>
>>
>> In your example we have
>>
>>    x :: forall a b. (T Int ~ b) => a
>>    x = False
>>
>> Think of the System F translation:
>>
>>    x = /\a b. \(d :: T Int ~ b). False |> ??
>>
>> Again, what evidence can we use to cast False to 'a'.
>>
>>
>> In short, fundeps and type family dependencies only add
extra
>> unification constraints, which may help to resolve
ambiguous
>> types.  They don’t provide evidence.  That's not to say
that they
>> couldn't.  But you'd need to extend System FC, GHC's core
language, to
>> do so.
>>
>> Simon
>>
>>
>>>
>>> -----Original Message-----
>>> From: Glasgow-haskell-users
[mailto:glasgow-haskell-users-
>>> bounces at haskell.org] On Behalf Of Wolfgang Jeltsch
>>> Sent: 05 July 2017 01:21
>>> To: glasgow-haskell-users at haskell.org
>>> Subject: Trouble with injective type families
>>>
>>> Hi!
>>>
>>> Injective type families as supported by GHC 8.0.1 do not
behave like
>>> I
>>> would expect them to behave from my intuitive
understanding.

>>>
>>> Let us consider the following example:
>>>
>>>>
>>>> {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
>>>>
>>>> class C a where
>>>>
>>>>     type T a = b | b -> a
>>>>
>>>> instance C Bool where
>>>>
>>>>     type T Bool = Int
>>>>
>>>> type X b = forall a . T a ~ b => a
>>>>
>>>> x :: X Int
>>>> x = False
>>> I would expect this code to be accepted. However, I get
the

>>> following
>>> error message:
>>>
>>>>
>>>> A.hs:14:5: error:
>>>>     • Could not deduce: a ~ Bool
>>>>       from the context: T a ~ Int
>>>>         bound by the type signature for:
>>>>                    x :: T a ~ Int => a
>>>>         at A.hs:13:1-10
>>>>       ‘a’ is a rigid type variable bound by
>>>>         the type signature for:
>>>>           x :: forall a. T a ~ Int => a
>>>>         at A.hs:11:19
>>>>     • In the expression: False
>>>>       In an equation for ‘x’: x = False
>>>>     • Relevant bindings include x :: a (bound at
A.hs:14:1)
>>> This is strange, since injectivity should exactly make
it possible

>>> to
>>> deduce a ~ Bool from T a ~ Int.
>>>
>>> Another example is this:
>>>
>>>>
>>>> {-# LANGUAGE GADTs, TypeFamilyDependencies #-}
>>>>
>>>> class C a where
>>>>
>>>>     type T a = b | b -> a
>>>>
>>>> instance C Bool where
>>>>
>>>>     type T Bool = Int
>>>>
>>>> data G b where
>>>>
>>>>     G :: Eq a => a -> G (T a)
>>>>
>>>> instance Eq (G b) where
>>>>
>>>>     G a1 == G a2 = a1 == a2a
>>> I would also expect this code to be accepted. However, I
get the
>>> following error message:
>>>
>>>>
>>>> B.hs:17:26: error:
>>>>     • Could not deduce: a1 ~ a
>>>>       from the context: (b ~ T a, Eq a)
>>>>         bound by a pattern with constructor:
>>>>                    G :: forall a. Eq a => a -> G (T
a),
>>>>                  in an equation for ‘==’
>>>>         at B.hs:17:5-8
>>>>       or from: (b ~ T a1, Eq a1)
>>>>         bound by a pattern with constructor:
>>>>                    G :: forall a. Eq a => a -> G (T
a),
>>>>                  in an equation for ‘==’
>>>>         at B.hs:17:13-16
>>>>       ‘a1’ is a rigid type variable bound by
>>>>         a pattern with constructor: G :: forall a. Eq a
=> a -> G
>>>> (T
>>>> a),
>>>>         in an equation for ‘==’
>>>>         at B.hs:17:13
>>>>       ‘a’ is a rigid type variable bound by
>>>>         a pattern with constructor: G :: forall a. Eq a
=> a -> G
>>>> (T
>>>> a),
>>>>         in an equation for ‘==’
>>>>         at B.hs:17:5
>>>>     • In the second argument of ‘(==)’,
namely ‘a2’
>>>>       In the expression: a1 == a2
>>>>       In an equation for ‘==’: (G a1) == (G
a2) = a1 == a2
>>>>     • Relevant bindings include
>>>>         a2 :: a1 (bound at B.hs:17:15)
>>>>         a1 :: a (bound at B.hs:17:7)
>>> If b ~ T a and b ~ T a1, then T a ~ T a1 and
subsequently a ~ a1,
>>> because
>>> of injectivity. Unfortunately, GHC does not join the two
contexts (b
>>> ~ T
>>> a, Eq a) and (b ~ T a1, Eq a1).
>>>
>>> Are these behaviors really intended, or are these bugs
showing up?
>>>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Trouble with injective type families

gkaracha
In reply to this post by Richard Eisenberg-4
Me and Tom Schrijvers recently got a paper accepted at Haskell '17 concerning the elaboration of functional dependencies in System FC without extending it:

    https://people.cs.kuleuven.be/~george.karachalias/papers/fundeps.pdf

The work is not currently implemented in GHC but we made some extra effort to make our system GHC-compatible so that integration will be possible in the future :-) In addition to the elaboration of FDs, we also noticed that they are unsound as currently implemented (Section 2.2 in the draft), if we treat them as type-level functions. Hence, we had to tighten up the restrictions imposed on them, good thing that until now they didn't affect the generated System FC code!

There is still some work to be done to transfer the results to injective type families but I believe we are getting there :)

Cheers,
George