Re: Heterogeneous equality

[Richard Eisenberg]

> On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch  wrote:
> 
> 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 don't believe it is, but (in my opinion) it should be.

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

Because the definition of heterogeneous equality requires polymorphic 
recursion, in that the usage of (:~~:) in the type of HRefl has different kind 
indices than the declaration head. Polymorphic recursion is allowed only when 
you have a *complete user-supplied kind signature*, as documented here 
(https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-user-supplied-kind-signatures-and-polymorphic-recursion).

This surprised me, too, when I first encountered it, but I believe it's the 
correct behavior.
Richard
___
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

[Anthony Clayden]

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