Inferring Recursive Types
Christopher Diggins
applies a function to itself.
\a.aa
I notice that SML 98 and F# can't infer the type (e.g. let M a = a a ).
What languages can infer the type? What language features are required
to express the type?
Why don't the type systems to those languages simply output something
like:
M : 'a.('a -> 'b) -> 'b
Thanks in advance,
Christopher Diggins
http://www.cdiggins.com
Mark T.B. Carroll
> let M a = a a
> Why don't the type systems to those languages simply output something
> like:
>
> M : 'a.('a -> 'b) -> 'b
Well, it's not that simple. The function a doesn't take an 'a as first
argument, it takes a function that takes, er, something with the same
signature as the function a, and outputs a b. The something is the
tricky bit - you get a sort of infinitely recursive type if you follow
the reasoning. Whether the languages' difficulty with this is a bug or a
feature, I don't know.
Mark.
--
Functional programming vacancy at http://www.aetion.com/
Benedikt Schmidt
> In Combinator theory the combinator SII (a.k.a. M or Mockingbird)
> applies a function to itself.
>
> \a.aa
>
> I notice that SML 98 and F# can't infer the type (e.g. let M a = a a ).
> What languages can infer the type?
Ocaml can with the rectypes option:
% ledit ocaml -rectypes
# fun a -> a a;;
- : ('a -> 'b as 'a) -> 'b = <fun>
> What language features are required to express the type?
Equi-recursive types where e.g. 'a list and 'a ('a list) are
considered equivalent types.
ML/Ocaml supports iso-recursive types where the user can define
type isomorphisms like
type intlist = Cons of int * intlist | Nil
and need explicit conversions between the types (fold/unfold) by
constructing (Cons 4 Nil) and deconstructing
(match l1 with Cons _ l2).
There is a chapter comparing the two in TaPL and some more
details are available in [1].
Benedikt
[1] http://cristal.inria.fr/~fpottier/publis/fpottier-appsem-2005.pdf
Andreas Rossberg
> In Combinator theory the combinator SII (a.k.a. M or Mockingbird)
> applies a function to itself.
>
> \a.aa
>
> I notice that SML 98 and F# can't infer the type (e.g. let M a = a a ).
> What languages can infer the type? What language features are required
> to express the type?
>
> Why don't the type systems to those languages simply output something
> like:
>
> M : 'a.('a -> 'b) -> 'b
I guess this is supposed to express the type
forall b. (forall a. a -> b) -> b
This is indeed (one) possible solution, but with its nested quantifier,
it is a so-called higher-rank polymorphic type. Plain ML does not allow
such types, because type inference for them is undecidable in general.
Some extensions to ML - i.e. Le Botlan/Remy's MLF, or Haskell with GHC
extensions - allow it if you supply sufficient type annotations. But the
meta-theory of such extensions is pretty involved, and more or less an
open research area.
Plain ML only supports prenex polymorphism, where all quantifiers are in
front. This is said to hit a "sweet spot" in type system design, because
it is expressive enough for most practical problems but still allows
complete type inference.
To type self application of an argument x in that system, you have to
solve the type equation
a = a->a'
To see why, assume x:t for some type t.
Because we apply something to x, we know t=t1->t2.
And because the argument also has type t, we need t1=t, i.e. t1=t1->t2.
The only solution is a recursive type, a fixed point of the above
equation. Usually this is written mu a.a->a'.
Such so-called equi-recursive types are not hard to add to ML, but the
thing is: You Do Not Want Them. Just recently, Andrew Bromage gave a
nice illustration why, on the Haskell-Cafe list:
http://www.haskell.org/pipermail/haskell-cafe/2006-December/020074.html
OCaml used to have recursive type inference in its very first versions,
but it was quickly banned to an explicit switch by popular demand.
Whenever you really need recursive types in ML, you can always express
them by explicit wrapping into an auxiliary algebraic datatype.
- Andreas
Christopher Diggins
illuminating and educational!
I have a perhaps naive inquiry given my new understanding: would you
destabilize a type-system if you pulled the qualifier to the front and
expressed the type using an overly general type? e.g. instead of
forall b. (forall a. a -> b) -> b
we wrote:
forall b. forall a. (a -> b) -> b
?
Also is the first solution not Rank-2 polymorphism? Pierce says in the
TaPL that rank-2 polymorphism is in fact decidable and rank-3 and
higher polymorphism is undecidable. Is the type inference of rank-2
polymorphism particularly hard I wonder? It seems to me that detecting
cylcical constraints should be relatively easy for a type inference
algorithm.
Anyway, thanks again for your help.
Thanks,
Christopher
Christopher Diggins
appreciated.
On Dec 21, 7:12 pm, Benedikt Schmidt <besc...@cloaked.de> wrote:
> "Christopher Diggins" <cdigg...@gmail.com> writes:
> > In Combinator theory the combinator SII (a.k.a. M or Mockingbird)
> > applies a function to itself.
>
> > \a.aa
>
> > I notice that SML 98 and F# can't infer the type (e.g. let M a = a a ).
> > What languages can infer the type?Ocaml can with the rectypes option:
> % ledit ocaml -rectypes
> # fun a -> a a;;
> - : ('a -> 'b as 'a) -> 'b = <fun>
>
> > What language features are required to express the type?Equi-recursive types where e.g. 'a list and 'a ('a list) are
ross...@ps.uni-sb.de
>
> I have a perhaps naive inquiry given my new understanding: would you
> destabilize a type-system if you pulled the qualifier to the front and
> expressed the type using an overly general type? e.g. instead of
>
> forall b. (forall a. a -> b) -> b
>
> we wrote:
>
> forall b. forall a. (a -> b) -> b
That is not a more general, it is a completely different type.
You can read forall in the same way as you read an arrow: it stands for
an argument, though a type, not a term argument. Considering that, the
difference between the two types above is analogous to the difference
between function types
c -> (d -> a -> b) -> b
and
c -> d -> (a -> b) -> b
You have inverted the roles of the function and its caller regarding
argument d, i.e. who is allowed to chose it. Same for type a above.
> Also is the first solution not Rank-2 polymorphism? Pierce says in the
> TaPL that rank-2 polymorphism is in fact decidable and rank-3 and
> higher polymorphism is undecidable. Is the type inference of rank-2
> polymorphism particularly hard I wonder?
Yes, your example is rank-2 (impredicative) polymorphism. Rank-2 is
decidable, but frankly I have no idea how the algorithm looks like.
- Andreas