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

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

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