Introducing Fran the Finite State Automaton

[compilerbitch]

Comments

[ashley-y.livejournal.com]

Hmm, if x has type α does that mean (Λ&beta. x) also has type α? If so I think I understand it.

[chard.livejournal.com]

Not quite. (Λβ. x) has type ∀β.α, where β is any symbol you like, of course. It has to be "applied" to a type. Normally in lambda-2 you write this kind of application differently (as a subscript) but I think this is silly, because some nested expressions get smaller and smaller, and you can usually tell whether it's a type or value application easily enough. Coo, I remember more than I thought.

[ashley-y.livejournal.com]

OK, when evaluating "cons int 4 (nil int)" I came across this, which confused me:

nil int : int list, where

nil int = Λβ . λb:β . λf:β→int→β . b
int list = ∀β.β→(β→int→β)→β

But it looks correct now.

[ashley-y.livejournal.com]

Why is it "α list" and not "list α"? Would this work:

list ::= Λα.∀β.β→(β→α→β)→β

...?

[chard.livejournal.com]

No reason. I'm one of the few people who's ever been a commercial ML programmer, and old habits die hard. You're right that it's nicer to just call this "list" and have it take a type.

I hope compilerbitch doesn't mind us filling up her journal with this nonsense.

[compilerbitch.livejournal.com]

No problem. Fill away!

:-)

I was paid to write Haskell for two whole weeks once...