Forgot to include the reference: [1] B. A. Yorgey et al. "Giving Haskell a Promotion" (http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf)
On Sep 3, 2012, at 3:26 PM, Richard Eisenberg wrote: > On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote: > >> As Edward and others have recognised, the problem here is that FC >> coercions are not expressive enough to prove eta rules, that is >> >> forall x : (a, b) . x ~ (Fst x, Snd x) >> >> or more generally, that every element of a single-constructor (record) >> type is equal to the constructor applied to the projections. >> >> It seems like it should be perfectly fine to assert such a thing as an >> axiom, though, ... unless >> you have Any (as Richard observed), in which case all bets are off. Why >> did you want Any again? > > > I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, > Any has been helpful in other type hackery exploits of mine...) So, any way > of introducing eta-coercions will have to respect Any. > > Intriguingly, the most recent published formulation of FC [1] leaves room for > adding eta rules. The issue is one of consistency: if we have a coercion g : > forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and the existence > of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for > consistency (from which progress & preservation are proved) apply only to > coercions at a base kind, either * or Constraint. So, our eta coercion g is > exempt from the consistency check -- it cannot make a system inconsistent. > Thus, with or without Any, the coercion g cannot lead to a program that > crashes due to a type error. > > So, it seems possible to introduce eta coercions into FC for all kinds > containing only one type constructor without sacrificing soundness. How the > type inference engine/source Haskell triggers the use of these coercions is > another matter, but there doesn't seem to be anything fundamentally wrong > with the idea. > > Richard _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
