[Haskell-cafe] There's nothing wrong with infinite types!

Stefan O'Rear stefanor at cox.net
Wed Dec 6 00:14:01 EST 2006

I'm sure anyone who's used Haskell for any significant length of time
has received this error message:

Occurs check: cannot construct the infinite type: t = t -> t1

I for one took that as a challenge, and have implemented a type
inference engine for infinite types.

Expr> s
(a -> b -> c) -> (a -> b) -> a -> c
Expr> skk
a -> a
Expr> s(skk)(skk)
(fix a . (a -> b))

Points of interest:

* There are NO error conditions.  it-unifier can assign a type to every
  syntactically valid expression of combinatory logic.

* Typechecking is guaranteed to terminate in a linear number of steps,
  an (apparently) stronger guarantee than that provided by DHM.

* (Mostly theoretical, since it-unify does not yet support sums or
  products): Fixpoint types subsume declared recursive datatypes.
  e.g: type List a = fix l . Either () (a,l)

darcs get http://members.cox.net/stefanor/fixtypes/

More information about the Haskell-Cafe mailing list