[Types-sig] how to do a typecase? (was: Static typing: Towards closure?)

Tim Peters tim_one@email.msn.com
Mon, 24 Jan 2000 02:13:13 -0500


[Jeremy Hylton]
> It isn't clear to me either, but I see that in Ocaml I can
> successfully evaluate:
>     "type node = Node of node | Int of int"
> but not
>     "let rec f () = f".
> This suggests to me that it is possible to allow recursive types
> without having a solution to latter problem.

FYI, the function example is a non-starter in Haskell, because Haskell has
no 0-argument functions (in a purely functional language, a 0-argument
function can never return different things on different calls, so they
generally don't allow for that -- you define a constant instead).

Here's a related Haskell example:  "f x = f".  In ocaml (I haven't used
that) you'd probably write something like "let rec f x = f;;" instead.

Type checking
ERROR "e:\hugs\ex.hs" (line 1): Type error in function binding
*** term           : f
*** type           : b -> a
*** does not match : a
*** because        : unification would give infinite type

"The rules" are spelled out in the Haskell reference.  I downloaded the
ocaml reference, and after failing to figure out *its* rules, bumped into
this paragraph:

    No attempt has been made at mathematical rigor:  words are
    employed with their intuitive meaning, without further
    definition.  As a consequence, the typing rules have been
    left out, by lack of the mathematical framework required
    to express them, while they are definitely part of a full
    formal definition of the language.

That's a real help <wink>.