Re: Explicit inequality evidence
Hi, I was thinking about (and almost needing) inequality evidence myself, so I’m :+1: to exploration. First the bike shedding: I’d prefer /~ and :/~:. -- new Typeable [1] would actually provide heterogenous equality: eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) And this one is tricky, should it be: eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) i.e. how kind inequality would work? -- I'm not sure about propagation rules, with inequality you have to be *very* careful! irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. I assume that in your rules, variables are not type families, otherwise x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x where F x = ()) other direction is true though. Also: f x ~ a -> b, is true with f ~ (->) a, x ~ b. -- Oleg - [1]: https://github.com/ghc-proposals/ghc-proposals/pull/16 > On 13 Dec 2016, at 06:34, David Feuer wrote: > > According to Ben Gamari's wiki page[1], the new Typeable is expected to offer > > eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a > :~: b) > > Ideally, we'd prefer to get either evidence of equality or evidence of > inequality. The traditional approach is to use Dec (a :~: b), where data Dec > a = Yes a | No (a -> Void). But a :~: b -> Void isn't strong enough for all > purposes. In particular, if we want to use inequality to drive type family > reduction, we could be in trouble. > > I'm wondering if we could expose inequality much as we expose equality. Under > an a # b constraint, GHC would recognize a and b as unequal. Some rules: > > Base rules > 1. f x # a -> b > 2. If C is a constructor, then C # f x and C # a -> b > 3. If C and D are distinct constructors, then C # D > > Propagation rules > 1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y) > 2. x # y <=> (x z) # (y z) <=> (z x) # (z y) > 3. If x # y then y # x > > Irreflexivity > 1. x # x is unsatisfiable (this rule would be used for checking patterns). > > With this hypothetical machinery in place, we could get something like > > data a :#: b where > Unequal :: a # b => Unequal (a :#: b) > > eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either (a > :#: b) (a :~: b) > > Pattern matching on an Unequal constructor would reveal the inequality, > allowing closed type families relying on it to reduce. > > Evidence structure: > > Whereas (:~:) has just one value, Refl, it would be possible to imagine > richer evidence of inequality. If two types are unequal, then they must be > unequal in some particular fashion. I conjecture that we don't actually gain > much value by using rich evidence here. If the types are Typeable, then we > can explore them ourselves, using eqTypeRep' recursively to locate one or > more differences. If they're not, I don't think we can track the source(s) of > inequality in a coherent fashion. The information we got would only be > suitable for use in an error message. So one option would be to bundle up > some strings describing the known mismatch, and warn the user very sternly > that they shouldn't try to do anything too terribly fancy with them. > > [1] https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs signature.asc Description: Message signed with OpenPGP using GPGMail ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: > First the bike shedding: I’d prefer /~ and :/~:. Those are indeed better. > new Typeable [1] would actually provide heterogenous equality: > > eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > TypeRep a -> TypeRep b -> Maybe (a :~~: b) > > And this one is tricky, should it be: > > eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). >TypeRep a -> TypeRep b -> >Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) > > i.e. how kind inequality would work? I don't know. It sounds like some details of how kinds are expressed in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe we should punt and use heterogeneous inequality? That's over my head. > I'm not sure about propagation rules, with inequality you have to be *very* > careful! > > irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. > > I assume that in your rules, variables are not type families, otherwise > > x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F > x where F x = ()) > other direction is true though. I was definitely imagining them as first-class types; your point that f x /~ f y => x /~ y even if f is a type family is an excellent one. > Also: > > f x ~ a -> b, is true with f ~ (->) a, x ~ b. Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just leave out that bogus piece. Thanks, David Feuer ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
I've thought about inequality on and off for years now, but it's a hard nut to crack. If we want this evidence to affect closed type family reduction, then we would need evidence of inequality in Core, and a brand-spanking-new type safety proof. I don't wish to discourage this inquiry, but I also don't think this battle will be won easily. Richard > On Dec 13, 2016, at 1:02 AM, David Feuer wrote: > > On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: >> First the bike shedding: I’d prefer /~ and :/~:. > > Those are indeed better. > >> new Typeable [1] would actually provide heterogenous equality: >> >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). >>TypeRep a -> TypeRep b -> Maybe (a :~~: b) >> >> And this one is tricky, should it be: >> >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). >> TypeRep a -> TypeRep b -> >> Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) >> >> i.e. how kind inequality would work? > > I don't know. It sounds like some details of how kinds are expressed > in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe > we should punt and use heterogeneous inequality? That's over my head. > >> I'm not sure about propagation rules, with inequality you have to be *very* >> careful! >> >> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. >> >> I assume that in your rules, variables are not type families, otherwise >> >> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family >> F x where F x = ()) >> other direction is true though. > > I was definitely imagining them as first-class types; your point that > f x /~ f y => x /~ y even if f is a type family is an excellent one. > >> Also: >> >> f x ~ a -> b, is true with f ~ (->) a, x ~ b. > > Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just > leave out that bogus piece. > > Thanks, > David Feuer > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
Possibly naive question: do we have decidable inequality in a meta theoretical sense? I feel like we have definite equality and fuzzy might not always be equal but could be for polymorphic types. And that definite inequality on non polymorphic terms is a lot smaller than what folks likely want? On Dec 13, 2016 10:01 AM, "Richard Eisenberg" wrote: > I've thought about inequality on and off for years now, but it's a hard > nut to crack. If we want this evidence to affect closed type family > reduction, then we would need evidence of inequality in Core, and a > brand-spanking-new type safety proof. I don't wish to discourage this > inquiry, but I also don't think this battle will be won easily. > > Richard > > > On Dec 13, 2016, at 1:02 AM, David Feuer wrote: > > > > On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus > wrote: > >> First the bike shedding: I’d prefer /~ and :/~:. > > > > Those are indeed better. > > > >> new Typeable [1] would actually provide heterogenous equality: > >> > >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > >>TypeRep a -> TypeRep b -> Maybe (a :~~: b) > >> > >> And this one is tricky, should it be: > >> > >> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). > >> TypeRep a -> TypeRep b -> > >> Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) > >> > >> i.e. how kind inequality would work? > > > > I don't know. It sounds like some details of how kinds are expressed > > in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe > > we should punt and use heterogeneous inequality? That's over my head. > > > >> I'm not sure about propagation rules, with inequality you have to be > *very* careful! > >> > >> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. > >> > >> I assume that in your rules, variables are not type families, otherwise > >> > >> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type > family F x where F x = ()) > >> other direction is true though. > > > > I was definitely imagining them as first-class types; your point that > > f x /~ f y => x /~ y even if f is a type family is an excellent one. > > > >> Also: > >> > >> f x ~ a -> b, is true with f ~ (->) a, x ~ b. > > > > Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just > > leave out that bogus piece. > > > > Thanks, > > David Feuer > > ___ > > ghc-devs mailing list > > ghc-devs@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
> On Dec 14, 2016, at 10:07 AM, Carter Schonwald > wrote: > > Possibly naive question: do we have decidable inequality in a meta > theoretical sense? I feel like we have definite equality and fuzzy might not > always be equal but could be for polymorphic types. And that definite > inequality on non polymorphic terms is a lot smaller than what folks likely > want? Not sure what you mean here. FC/Core has a definitional equality which is decidable (and must be). And if definitional equality is decidable, it follows that definitional inequality is decidable. On the other hand, what we are talking about in this thread is *propositional* inequality -- that is, an inequality supported by a proof. Propositional equality must be a larger relation than definitional equality: this is what the Refl constructor, or in the Greek, shows. It then follows that propositional inequality must be smaller than definitional inequality. This is a Good Thing, because F Int and Bool are definitionally inequal, but we don't want them to be propositionally inequal. Propositional inequality is almost surely undecidable, because of looping type families (at least). But that's OK -- propositional equality is also undecidable, and that hasn't slowed us down. :) Richard ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
Out of curiosity: where's the current type safety proof, and is it mechanized? Oleg On 13.12.2016 17:01, Richard Eisenberg wrote: > I've thought about inequality on and off for years now, but it's a hard nut > to crack. If we want this evidence to affect closed type family reduction, > then we would need evidence of inequality in Core, and a brand-spanking-new > type safety proof. I don't wish to discourage this inquiry, but I also don't > think this battle will be won easily. > > Richard > >> On Dec 13, 2016, at 1:02 AM, David Feuer wrote: >> >> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: >>> First the bike shedding: I’d prefer /~ and :/~:. >> Those are indeed better. >> >>> new Typeable [1] would actually provide heterogenous equality: >>> >>> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). >>>TypeRep a -> TypeRep b -> Maybe (a :~~: b) >>> >>> And this one is tricky, should it be: >>> >>> eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2). >>> TypeRep a -> TypeRep b -> >>> Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b) >>> >>> i.e. how kind inequality would work? >> I don't know. It sounds like some details of how kinds are expressed >> in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe >> we should punt and use heterogeneous inequality? That's over my head. >> >>> I'm not sure about propagation rules, with inequality you have to be *very* >>> careful! >>> >>> irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear. >>> >>> I assume that in your rules, variables are not type families, otherwise >>> >>> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family >>> F x where F x = ()) >>> other direction is true though. >> I was definitely imagining them as first-class types; your point that >> f x /~ f y => x /~ y even if f is a type family is an excellent one. >> >>> Also: >>> >>> f x ~ a -> b, is true with f ~ (->) a, x ~ b. >> Whoops! Yeah, I momentarily forgot that (->) is a constructor. Just >> leave out that bogus piece. >> >> Thanks, >> David Feuer >> ___ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > signature.asc Description: OpenPGP digital signature ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
Hi Oleg,
I'm afraid to say that there is no one current type safety proof. Instead,
there are lots of bits and pieces:
- A system with roles (but no TypeInType or kind polymorphism) is proved in
"Safe Zero-cost Coercions for Haskell" (JFP '16) [1].
- A system with TypeInType but no roles is proved in "System FC with Explicit
Kind Equality (extended version)" (ICFP '13) [2]. This type safety proof is
broken (see [3], section 5.10.5.2), but we have no counterexample to safety.
- Closed type families are proved safe in "Closed Type Families with
Overlapping Equations" (POPL '14) [4]. This system has no roles nor kind
polymorphism. It also assumed that type family reductions terminate, explicitly
leaving the challenge of proving safety with non-terminating type families as
an open problem (see Section 6 of that paper). There may be a solution in work
that has since been completed ("Non-ω-overlapping TRSs are UN" (LIPIcs '16)
[5]), but I'm not aware of work that has adapted that solution to work with
Haskell.
- My thesis (Univ. of Pennsylvania '16) [3] has a proof of a version of Haskell
with dependent types. Closed type families have been converted into type-level
lambdas; the full proof does not consider the possibility of non-linear
patterns in type families. A start toward such an approach is described
(Section 5.13.2) but not fleshed out. Roles are not included.
- A draft paper, never published, ("An overabundance of equality: Implementing
kind equalities into Haskell" (2015) [6]) considers the possibility of
combining roles with TypeInType. The proof is somewhat sparse, and it has not
gotten the level of scrutiny in the other proofs. Furthermore, the way roles
and TypeInType are integrated in GHC is different than what appears in this
draft.
- Forthcoming work, by Stephanie Weirich, Pedro Amorim, Antoine Voizard, and
myself, contains a mechanized proof of safety of a dependently typed
Haskell-like system, but with no roles, closed type families, or even
datatypes. I do not believe there is a public link to this work; we expect to
submit to ICFP.
- There is a formally written, but unproved, description of what is implemented
in GHC [7]. It is useful for understanding the GHC source code in relation to
other published work. There is no proof whatsoever.
This is a sorry state of affairs, I know. It remains my hope that we will have
a formal, mechanized proof of this all Some Day, and progress is indeed slowly
marching toward that goal.
Richard
[1]: http://cs.brynmawr.edu/~rae/papers/2016/coercible-jfp/coercible-jfp.pdf
[2]: http://cs.brynmawr.edu/~rae/papers/2013/fckinds/fckinds-extended.pdf
[3]: http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf
[4]: http://cs.brynmawr.edu/~rae/papers/2014/axioms/axioms-extended.pdf
[5]: http://kar.kent.ac.uk/55349/1/proc-kahrs.pdf
[6]: http://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf
[7]: https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf
> On Dec 15, 2016, at 1:30 AM, Oleg Grenrus wrote:
>
> Out of curiosity: where's the current type safety proof, and is it
> mechanized?
>
> Oleg
>
>
> On 13.12.2016 17:01, Richard Eisenberg wrote:
>> I've thought about inequality on and off for years now, but it's a hard nut
>> to crack. If we want this evidence to affect closed type family reduction,
>> then we would need evidence of inequality in Core, and a brand-spanking-new
>> type safety proof. I don't wish to discourage this inquiry, but I also don't
>> think this battle will be won easily.
>>
>> Richard
>>
>>> On Dec 13, 2016, at 1:02 AM, David Feuer wrote:
>>>
>>> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote:
First the bike shedding: I’d prefer /~ and :/~:.
>>> Those are indeed better.
>>>
new Typeable [1] would actually provide heterogenous equality:
eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
And this one is tricky, should it be:
eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b ->
Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b)
i.e. how kind inequality would work?
>>> I don't know. It sounds like some details of how kinds are expressed
>>> in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe
>>> we should punt and use heterogeneous inequality? That's over my head.
>>>
I'm not sure about propagation rules, with inequality you have to be
*very* careful!
irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear.
I assume that in your rules, variables are not type families, otherwise
x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type
family F x where F x = ())
other direction is true though.
>>> I was definitely imagining them as first-class types; your point that
>>> f x /~ f y => x /~ y even if f is a type family is an excellent o
