Release plans

[Brandon Michael Moore]

Sending to the right list this time, with some additions.

> Just to show what kind of problems we are currently facing. The  
> following type checks in our EHC compiler and in Hugs, but not in the  
> GHC:
> 
> module Test where
> 
> data T s = forall x. T (s -> (x -> s) -> (x, s, Int))
> 
> run :: (forall s . T s) -> Int
> run ts  = case ts of
>             T g -> let (x,_, b) =  g x id
>                    in b

Consider this additional code which also typechecks in Hugs:

v :: forall s . T s
v = T f

f :: s -> ([s] -> s) -> ([s], s, Int)
f v g = let x = [v] in (x, g x, 0)

run v gives 0. Apparently id has type [s] -> s. I'm not sure
if we're ending up with the infinite type s = [s], or maybe
something really bad would happen in run v, if it were not
for parametricity keeping us from examining the first two
elements of the triple too closely (I tried adding Show
constraints, but couldn't get code like that to typecheck).

Now for wild speculation:

Simplifing T and assuming full existentials, you might define
something akin to run with a type like
(forall s . exists x. (x -> s) -> (x, s))
 -> (exists t . (t -> t) -> (t, t)),
which suggest to me two ingredients (in a language with type operators),
a functional axiom of choice plus fixpoints of type operators,
ac :: (forall a . exists b. X) -> exists f::*->*. forall a . X[f(a)/b]
and fixT :: (* -> *) -> *

Then you might implement the type above as

equalize pkg =
  open ac pkg as {exists F. body}
  in close {fixT F, body}

Brandon