[Haskell-cafe] Re: Mysterious fact

[Jon Fairbairn]

Andrew Coppin <andrewcoppin at btinternet.com> writes:

> The other day, I accidentally came up with this:
>
> |{-# LANGUAGE RankNTypes #-}
>
> type  Either  x y=  forall r.  (x ->  r) ->  (y ->  r) ->  r
>
> left :: x ->  Either  x y
> left x f g=  f x
>
> right :: y ->  Either  x y
> right y f g=  g y
>
> |
>
> This is one example; it seems that just about any algebraic
> type can be encoded this way. I presume that somebody else
> has thought of this before. Does it have a name?

You could try reading my PhD thesis!
<http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-75.html>
contains a link to the full text scanned to a pdf. (That -- 1985
-- was a long time ago. One thing I really regret about it is
that there should have been a comma between "simple" and "typed"
in the title. I suspect people think "simply typed" when they
see it). It isn't hard to read (one of my examiners said it made
good bed-time reading).

Anyway, the relevant part is that Ponder was a programming
language (Stuart Wray even wrote a GUI programme in it) that had
(in principle) no built-in types, relying on the type system
being powerful enough to express anything and the optimiser
being good enough to convert them to something more sensible.
In practice neither was /quite/ true, but it got quite close.

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk
http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html  (updated 2010-09-14)