(no subject)

Date: 2004-12-15 07:55 am (UTC)
From: [identity profile] chard.livejournal.com

Consider




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

cons ::= Λα. λa:α . λr:α list . Λβ . λb:β . λf:β→α→β . r β (f b a) f

nil ::= Λα. Λβ . λb:β . λf:β→α→β . b



list ::= cons int 1 (cons int 2 (cons int 3 (cons int 4 (nil int))))


then



list int 0 +


yields 10.



Phew! It's a long time since I did any lambda-2. Neurons aching. Eek!

(no subject)

Date: 2004-12-15 08:11 am (UTC)
From: [identity profile] compilerbitch.livejournal.com
Yerrrrrsss, but it's pushing it a bit to call that a loop!

Actually I agonised over the punchline for quite a while, and decided to go for the version I used because it was the funniest, even though I felt I should have been a bit more rigorous with Tim's definition.

I have plans for a new character, Yvonne, for a future cartoon. I think she will get on with Tim rather well. She'll definitely be able to bring something that's been missing in his life. If you see what I mean...

(no subject)

Date: 2004-12-15 08:25 am (UTC)
From: [identity profile] ashley-y.livejournal.com
I'm sure she'll be a fixture in his life.

(no subject)

Date: 2004-12-15 08:43 am (UTC)

(no subject)

Date: 2004-12-15 09:30 am (UTC)
From: [identity profile] chard.livejournal.com
Yerrrrrsss, but it's pushing it a bit to call that a loop!


Oh, I don' t know, it has all the attributes of a loop like for item in list or even node = list; while(node != NULL) { f(node); node = node->next; } or anything which "loops" over a data structure. I don't know about you but I hardly ever write any other kind of loop. The only thing this kind of programming can't capture is indefinite loops, but who writes those except in servers? Oh, and GUI apps with event streams. Hmmm…



I don't know if I should admit this, but I spent many days (spread over several years) translating commonplace programs into lambda-2 just to show it could be done. The damaging effects are with me even now.



She'll definitely be able to bring something that's been missing in his life. If you see what I mean...


But I'll bet she's a bit paradoxical ;-)

(no subject)

Date: 2004-12-15 03:47 pm (UTC)
From: [identity profile] chard.livejournal.com

Funnily enough, on my walk home I was trying to think of how to represent this as a comic strip. In most languages the loop is the active bit, and the data structure is passive. So it's like having a creature (perhaps a fluffy!) running over the data structure and applying the function/loop body to each part of it. But in lambda-2 a data structure is the active thing that applies a function over itself, so I imagined a fluffy who applies the function to himself and then passes it on to his friends. In this case he's holding hands with one other fluffy and the function is a hula-hoop that turns him from from a fluffy into something else when he steps through. Then I remembered that fluffies don't have hands.



Have you read "Tales of the Beanworld" by Larry Marder?

(no subject)

Date: 2004-12-15 08:20 am (UTC)
From: [identity profile] ashley-y.livejournal.com
Hmm, if x has type α does that mean (Λ&beta. x) also has type α? If so I think I understand it.

(no subject)

Date: 2004-12-15 09:37 am (UTC)
From: [identity profile] 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.

(no subject)

Date: 2004-12-15 09:45 am (UTC)
From: [identity profile] 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.

(no subject)

Date: 2004-12-15 09:47 am (UTC)
From: [identity profile] ashley-y.livejournal.com
Why is it "α list" and not "list α"? Would this work:

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

...?

(no subject)

Date: 2004-12-15 03:41 pm (UTC)
From: [identity profile] 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 [livejournal.com profile] compilerbitch doesn't mind us filling up her journal with this nonsense.

(no subject)

Date: 2004-12-16 02:04 am (UTC)
From: [identity profile] compilerbitch.livejournal.com
No problem. Fill away!

:-)

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

Profile

compilerbitch: That's me, that is! (Default)
compilerbitch

January 2016

S M T W T F S
     12
3 45 6789
10111213 141516
17181920212223
24 252627282930
31      
Page generated Sep. 10th, 2025 11:45 am

Style Credit

Expand Cut Tags

No cut tags