foundational question
Sean McIlroy
it is easy to convince oneself that the function id
(id x) = x
is such that ((id id) x)==(id x) evaluates as True for any x,
confirming the expectation that (id id) = id. this observation
suggests the following argument:
let f be any function whose principal type, like that of id, is (s ->
s). since (t -> t) -> u is a substitution instance of (s -> s) iff u =
(t -> t), f has type (t -> t) -> u iff u = (t -> t). hence (f f) is
welldefined and has principal type (t -> t) = (s -> s). hence one
ought to be able to define
selfapply :: (s -> s) -> (s -> s)
selfapply f = (f f)
but my interpreter (winhugs) complains that "unification would give
infinite type", and i'm not completely unsympathetic to its point of
view: if f has type s, and (f f) has type t, then the application of
the function f (of type s) to the argument f (of type s) is an
expression (f f) of type t; hence f has type (s -> t), implying the
infinite regress
s = (s -> t) = ((s -> t) -> t) = etc
what is the resolution of this paradox? should the proposed definition
of selfapply be permissible? why (not)? thanks if you can shed any
light on this.
peace
stm
Mark T.B. Carroll
> selfapply :: (s -> s) -> (s -> s)
> selfapply f = (f f)
>
> but my interpreter (winhugs) complains that "unification would give
> infinite type"
Does selfapply f = f . f do what you want?
Mark
Dirk Thierbach
> let f be any function whose principal type, like that of id, is (s -> s).
BTW, one can show that in the lambda calculus, there's only one function
with principal type s -> s, namely "id".
> since (t -> t) -> u is a substitution instance of (s -> s) iff u =
> (t -> t), f has type (t -> t) -> u iff u = (t -> t). hence (f f) is
> welldefined
That depends a bit on how exactly you want to introduce f here. It's
easier to see the distinction if one makes the quantification of type
variables explicit: If f is a function that's already defined (or
equivalently, if f is introduced by a let-binding), then f has the
fully polymorphic type
f :: forall s. s -> s
In that case one can type (f f) by instantiating the first f with
s = t -> t and the second f with s = t. Hence the first f has type
(t -> t) -> (t -> t), the second has type (t -> t), and the whole
application has also type (t -> t).
OTOH, if you use f as an argument to a function as below, i.e.
selfapply :: forall s. ((s -> s) -> (s -> s))
and don't give f a higher-rank type explicitely, then the first f and
the second f share the type variable s. To type the application, the
type s -> s of the second f used as argument must be unified with the
type s of the argument expected for the first f. This unification can
only be resolved by a recursive type, which doesn't exist in this way
in Haskell.
With an explicit higher rank type it works (in GHC, not sure about
WinHugs). Note the LANGUAGE option:
{-# LANGUAGE Rank2Types #-}
selfapply :: (forall s. s -> s) -> (t -> t)
selfapply f = (f f)
*Main> :r
[1 of 1] Compiling Main ( xxx.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t selfapply id
selfapply id :: t -> t
> and has principal type (t -> t) = (s -> s). hence one
> ought to be able to define
>
> selfapply :: (s -> s) -> (s -> s)
> selfapply f = (f f)
> but my interpreter (winhugs) complains that "unification would give
> infinite type",
Yes, that's correct :-)
> what is the resolution of this paradox?
Does the above explanation resolve it?
> should the proposed definition of selfapply be permissible?
No, unless one wants to allow (direct) recursive types.
> why (not)?
Because in Haskell, recursive types always must have one datatype
constructor "in between". It's actually possibly to have a type system
with full (direct) recursive types (OCaml allows this with a compiler
option, for example). But the practical experience is that this is
rarely useful on the one hand, and on the other hand there are now
many expressions typeable which arise from obvious programming mistakes,
so the type system is a lot less useful in helping to avoid errors.
Hence, it's normally not worth it.
> thanks if you can shed any light on this.
HTH,
- Dirk
Sean McIlroy
wrote:
it does help. thanks. do you have a reference for the lambda-calculus
theorem you mention? i'd be very interested to know the details.
peace
stm
Paul Rubin
> > BTW, one can show that in the lambda calculus, there's only one function
> > with principal type s -> s, namely "id".
> theorem you mention? i'd be very interested to know the details.
There is a whole mini-subject surrounding this:
http://citeseer.ist.psu.edu/wadler89theorems.html
Note that it doesn't necessarily apply in the presence of 'seq':
http://wwwtcs.inf.tu-dresden.de/~voigt/p76-voigtlaender.pdf
http://wwwtcs.inf.tu-dresden.de/~voigt/seqFinal.pdf
Dirk Thierbach
> it does help. thanks. do you have a reference for the lambda-calculus
> theorem you mention?
Sorry, I've forgotten the details. Informally, one can reason that
since the typing s -> s must be valid for any type s, the function
in question cannot assume anything about the type of the argument,
so there's little one can do with it except return it eventually.
And it can't return anything else, because it has to return something
with the same type as the argument.
I *think* the formal proof works with the semantic side (because
extensionality must play a role), but as said, my memory is foggy.
It's been some time since that course :-)
- Dirk