[plt-scheme] Recursive types and their specification

On Aug 9, 2005, at 11:44 AM, Noel Welsh wrote:

>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
>
>
> --- Robby Findler <robby at cs.uchicago.edu> wrote:
>
>> Did you try using a datatype to do that?
>
> Nope.  Being a faithful student of HtDP I decorate my
> Scheme programs with type declarations in the comments, so
> this question arose from Scheme programming, not <your
> favourite statically typed FPL>.  I couldn't see a way to
> write down the type without going introducing extra
> machinery

The HTDP approach super-imposes a type system on Scheme but allows for 
Scheme-ish programming puns on rare occasion.

Starting with Part II you are defining recursive types all the time. 
The one that you describe is one too, except that you don't go through 
a plain constructor. Instead you are going through an arrow constructor 
and therefore the definition doesn't need a base case:

An Action is a a function
  input: none
  outputs: an Action, a value (symbol, string, number)

When you use shorthand, this becomes

  Action = Unit -> Action Symbol

[I am using juxtaposition to denote multiple values here.]

If you wanted to use a formal type system, you wouldn't use equations 
per se. Instead you'd use

  (RecursiveType Action (Unit . ->* . Action Symbol))

[I am borrowing Spidey-like notation here.]

And this connects HtDP to Matthew's response. -- Matthias


>
> --- Matthew Flatt <mflatt at cs.utah.edu> wrote:
>
>> Yes. As your subject line says, the problem is a
>> equi-recursive function type
>>
>>   mu x . () -> (action * x)
>>
>> which is not in the type system.
>>
>
> Thanks.  This is interesting.  Had I the time, I'd read
> more about this (Google turns up some interesting hits); as
> it is, back to Pacman.
>
> Cheers,
> Noel
>
> Email: noelwelsh <at> yahoo <dot> com   noel <at> untyped <dot> com
> AIM: noelhwelsh
> Blogs: http://monospaced.blogspot.com/  
> http://www.untyped.com/untyping/
>
> __________________________________________________
> Do You Yahoo!?
> Tired of spam?  Yahoo! Mail has the best spam protection around
> http://mail.yahoo.com
>