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

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 wrote:

On Wed, Mar 19, 2008 at 12:48 AM, Benjamin L. Russell 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