Heterogeneous equality

[Wolfgang Jeltsch]

Hi!

The base package contains the module Data.Type.Equality, which contains
the type (:~:) for homogeneous equality. I was a bit surprised that
there is no type for heterogeneous equality there. Is there such a type
somewhere else in the standard library?

I tried to define a type for heterogeneous equality myself as follows:

> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> 
> data a :~~: b where
> 
> HRefl :: a :~~: a

To my surprise, the kind of (:~~:) defined this way is k -> k -> *, not
k -> l -> *. Why is this? Apparently, the latter, more general, kind is
possible, since we can define (:~~:) :: k -> l -> * as follows:

> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> 
> data (a :: k) :~~: (b :: l) where
> 
> HRefl :: a :~~: a

All the best,
Wolfgang
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Trouble with injective type families

[Richard Eisenberg]

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  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 + 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-
>>> boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
>>> Sent: 05 July 2017 01:21
>>> To: glasgow-haskell-users@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 

Re: Trouble with injective type families

[Wolfgang Jeltsch]

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 + 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-
> > boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
> > Sent: 05 July 2017 01:21
> > To: glasgow-haskell-users@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
> > >  

RE: Trouble with injective type families

[Simon Peyton Jones via Glasgow-haskell-users]

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-
| boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
| Sent: 05 July 2017 01:21
| To: glasgow-haskell-users@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?
| 
| All the best,
| Wolfgang
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
| ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-
|