[I hear cries of Haskell 2] Phil Wadler writes: > The suggestion is: > > Remove the restriction that type synonym > declarations must not be recursive. > > [...] > > The obvious way to go is for someone to implement it first, to > make sure it's not difficult. Mark Jones, have you tried this > in Gofer yet? It's not a big deal if you use a graph algorithm for unification -- you just don't bother checking whether the result of unification is recursive! I implemented recursive types this way in 1987, and I'm sure this wasn't new then. A graph algorithm is arguably the "right way" to implement type inference, anyway (Patrick Sansom has achieved significant speedup for type inference in GHC by adopting a graph-based algorithm). I have a paper in the 1991 Glasgow FP Workshop which describes this algorithm in a functional style K. Hammond, "Efficient Type Inference Using Monads", Proc 1991 Glasgow Workshop on Functional Programming, Portree, Skye, 1991, Springer-Verlag Series of Workshops in Computing Science. and adds the occurs check to obtain normal types. The same thing is also sketched out in my thesis (as a programming example for DACTL). It is slightly harder to do with substitutions, but to compensate you can remove the horrible occurs check. I don't know the state of theoretical work on substitutions for recursive types. Anyone? The really big issue is how you represent recursive types for printing or to define new types. Coming from a graph rewriting world, I prefer explicit labelling (with type variables as labels) to implicit recursion via synonyms. For example e :: a:(Int -> a) defines "e" to have the recursive type (Int -> Int -> ....). If you think in terms of mu types, this is just syntactic sugar for: e :: mu a . Int -> a There's a nice relationship between types represented this way and graph-based unification. The other nice things about using explicit labels rather than implicit synonyms are that 1) They can be used in arbitrary signatures without needing to predeclare type synonyms. 2) They have a uniform printable representation (not true for synonyms, since you might be able to unify a type with more than one synonym). 3) With the right algorithm, it's easy to generate recursive types -- which makes type inference straightforward (essentially you *remove* the "occurs check" but make sure you "tie a knot" at this point -- trivial with a graph, slightly harder with substitutions). 4) It's easy to introduce multiple recursions in the same type (you need multiple mutually recursive synonyms to achieve the same effect): e :: a: ((b:Int -> Char -> b) -> a) The big disadvantage of recursive types seems to be that you may not be able to detect when a function is applied to the wrong number of arguments, since a type variable will now unify with a recursive function type: f :: a -> a unifies with f :: a -> a: (b -> b) Either John Launchbury or Simon Marlow had a convincing example of how this could cause problems. Kevin

- Recursive type synonyms wadler
- Re: Recursive type synonyms Joe Fasel
- Re: Recursive type synonyms jones-mark
- Re: Recursive type synonyms jones-mark
- Re: Recursive type synonyms Alastair Reid
- Re: Recursive type synonyms wadler
- Re: Recursive type synonyms kh
- Re: Recursive type synonyms smk
- Re: Recursive type synonyms John Hughes
- Recursive type synonyms Varol Akman
- Re: Recursive type synonyms wadler
- Re: Recursive type synonyms Chris M P Reade