I had some more ideas on Tim Sweeney's thoughts:
First of all, I was releaved to see that the definition can be
extended to
b ^^ 0 = 1
(a functional programmer's favourite number must be zero!),
or for types
void --> t ~= unit
> Now I am trying to understand the type-theory analogy to tetration. Given
> "unit" as the one-valued type, "bool" as the two-valued type, "three" as the
> three-valued type (isomorphic to "maybe bool"), etc., clearly:
I find it hard to believe that the size of a flat domain can make such
a difference. I find (), Maybe (), Maybe (Maybe ()), ..., which are
not flat, more promising candidates. (Or Void, Maybe Void, ....)
Still I doubt there can be a type constructor Tetra with
Tetra () t ~= t and
Tetra (Maybe n) t ~= (Tetra n t) -> t,
although I couldn't disprove it.
It should reflect arithmetic laws of tetration, which for example
relate (b ^^ (a1*a2)) with b^^a1 and b^^a2 or so, but are there any?
So how should (a,b)-->t be defined?
Nevertheless we can nearly do it in Haskell, it's not legal, but the
intended meaning should be clear ;-)
First of all, we use church numerals at the type constructor level -
not my idea, must have seen it in some paper:
Z :: (* -> *) -> * -> *
type Z f x = x
S :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *
type S n f x = f (n f x)
Now we can define Tetra as
type Tetra t n = n (->t) ()
just as we could define (^^) as
b ^^ n = foldnat (b^) 1 n
only that the fold is already built into the numerals.
Tetra hasn't kind * -> * -> *, but has * -> ((* -> *) -> * -> *) -> *.
Now we'd have Tetra t Z = (), Tetra t (S Z) = () -> t ~= t,
Tetra t (S (S Z)) = (() -> t) -> t ~= t -> t and so on.
The problems with this are: Haskell has no kind signatures, so Z gets
kind * -> * -> *, you can't write (->t), and you can't use a type
synonym without giving all its arguments.
Still it could be instructive to ask yourself what other constructors
of kind (*->*)->*->* you might use, and what you'd get. Most
interessting should be Infinity:
type Inf f x = f (Inf f x)
(where we use x to get the correct kind) - this recursive type synonym
is even more forbidden!
> unit-->t ~= t
> bool-->t ~= t->t
> three-->t ~= (t->t)->t
> four-->t ~= ((t->t)->t)->t
>
> So, what is going on here? "bool->t" is the type of identity functions on
> t; "three-->t" is especially interesting because it is the type of fixpoint
> operator from t->t to t.
It's interesting (for those to which this wasn't obvious) to see that
there exists a recursion- und bottom-free term (this is what type
theory usually is about) of type n-->t (where n is a number) iff
n is even:
For n=2 there is id::t->t (or const id :: (() -> t) -> t, if you use
this) - or if you take my advice and start with zero, there is ()::().
Now if you have f::n-->t, then ($f) has type (n-->t)->t'->t', which is
even more general than (n+2)-->t.
We know there is no term of type t = 1-->t.
[For the following argument I first wanted to use the
Curry-Howard-Isomorphism, but then I realized I could show it
direct. Do I need it if I wanted to rigourously prove there is no term
of type t?]
Consider there were a term f of type n-->t = ((n-1)-->t) -> t with odd n>=3.
We already know there is a term h of type (n-1)-->t,
so the application f h would have type t, which is impossible.
Of course it is different if you take a fixed non-void type for t.
For example, ($0) has type (more general than) 3-->Int.
Bye,
Christian
