Re: Tetration operator in functional programming

[Christian Sievers]

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