On Monday 01 November 2010 6:40:30 pm Jeremy Shaw wrote: > Looks a lot like Church encoding to me: > > http://en.wikipedia.org/wiki/Church_encoding > > It was first discovered by the guy who invented lambda calculus :p
Also, if you're interested in this, you can read Proofs and Types by Girard (not an easy read). In it, (I think) he notes, and probably proves, that you can encode any inductive type in System F (which is relatively close to Haskell with rank-n types) by this method (that is, it has the right types; of course it works in the untyped lambda calculus, too, but not in, say, the simply typed lambda calculus). You can also encode coinductive types: nu F = exists s. s * (s -> F s) exists s. T[s] = forall r. (forall s. T[s] -> r) -> r -- Dan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe