[Haskell-cafe] Any ideas for "->" (function type) in a simply-typed lambda calculus version of Brett Victor's Alligator Eggs game?

[Benjamin L. Russell]

I like your idea of joining alligator tails to
represent the connective, but just came up with a
different idea about representing types.

The difficulty with using alligator sizes to represent
types is that deciding how to represent relationships
between types could pose a problem.  For example,
suppose I have a function lengthOfAddedList, which
takes a Char and a list, and returns the length of the
list with the Char prepended:

lengthOfAddedList.hs:
lengthOfAddedList :: Char -> [Char] -> Int
lengthOfAddedList c cs = length([c]++cs)

If we represent types as sizes, then, we can have,
say, Char having a smallest size, [Char] having a size
one size larger than Char, and Int having a size one
size still larger than [Char].

But then, how do we represent the difference in
relationships between the Char and [Char], and the
[Char] and Int?  A [Char] is a list of Chars, but an
Int is an unrelated type.

Further, suppose we have the following function:

lengthOfAddedListWithBool.hs:
lengthOfAddedListWithBool :: Bool -> [Bool] -> Int
lengthOfAddedListWithBool b bs = length([b]++bs)

How do I decide whether Char or Bool has a larger
alligator size, and how do I motivate this decision? 
Again, it is not clear.

Therefore, I propose that types be represented by
patterns (as it stripes vs. dots vs. a checkered
pattern, etc.) instead of sizes.  I.e., the Char type
can be represented by a striped pattern on an
alligator, the Bool type can be represented by a
striped pattern, and so on.

Then, we can establish the rule that putting a type in
a list is represented by putting that pattern in bold
on the alligator, so we can have 

lengthOfAddedList :: Char -> [Char] -> Int

be represented by an alligator with a striped pattern
tying its tail to an alligator with a bold striped
pattern tying its tail to an alligator with, say, dots
(assuming dots represent the Int type), and we can
have 

lengthOfAddedListWithBool :: Bool -> [Bool] -> Int

be represented by an alligator with a checkered
pattern tying its tail to an alligator with a bold
checkered pattern tying its tail to an alligator with
dots.

Patterns would seem to allow more freedom of
expression in denoting relationships between types
(say, a type of a list of Chars to a type of a Char)
than sizes.

There are probably even better ways of representing
relationships between types on alligators.

This seems a good start; what do you think?

Benjamin L. Russell

--- Justin Bailey <jgbailey at gmail.com> wrote:

> On Wed, Mar 19, 2008 at 12:48 AM, Benjamin L.
> Russell
> <dekudekuplex at yahoo.com> wrote:
> >  However, in thinking about how to adapt the game,
> I am
> >  not quite sure how to incorporate the
> representation
> >  of "->" (function type):
> >
> >  * ???:  "->" (function type)
> >
> >  What ideas, if any, would anybody have on how
> "->"
> >  (function type) could be represented in a
> simply-typed
> >  lambda calculus version of Brett Victor's
> Alligator
> >  Eggs?
> 
> Since color is already taken, how about representing
> types as skinny
> and fat alligators? Functions can then be
> represented by alligators
> with their tails joined together. For example, Nat
> -> Bool would be
> represented as a skinny alligator joined to a fat
> alligator. A skinny
> alligator will only eat anotehr skinny alligator,
> and then goes to
> take a nap (i.e. disappears). That leaves the fat
> alligator (bool).
> Just a sketch but maybe it will help you out!
> 
> Justin
>