Discussion:
SML question
(too old to reply)
Fernando
2010-09-07 21:10:39 UTC
Permalink
Dear guys,

I am trying to simulate booleans in lambda calculus. I am using
SML to play with the concept, but I am getting an error that I can't
understand:

Consider these definitions:

- val T = fn x => fn y => x;
- val F = fn x => fn y => y;
- val NOT = fn x => x F T;
- val XOR = fn a => fn b => a (NOT b) b;

We see that:

XOR T F true false

works without any problem. It returns the right answer 'true'.
however, when I try:

XOR F T true false;

I get this error:

stdIn:30.1-30.19 Error: operator and operand don't agree [tycon
mismatch]
operator domain: 'Z -> 'Y -> 'Y
operand: bool
in expression:
((XOR F) T) true

Even though:

F F T true false produces the expected answer. Why does it happen?

All the best,

Fernando
Bart Kastermans
2010-09-10 17:06:08 UTC
Permalink
Post by Fernando
Dear guys,
I am trying to simulate booleans in lambda calculus. I am using
SML to play with the concept, but I am getting an error that I can't
The basic difference is that the lambda calculus is not typed. And
your example shows what happens with these definitions in a typed
context.
Post by Fernando
- val T = fn x => fn y => x;
- val F = fn x => fn y => y;
- val NOT = fn x => x F T;
- val XOR = fn a => fn b => a (NOT b) b;
XOR T F true false
works without any problem. It returns the right answer 'true'.
XOR F T true false;
stdIn:30.1-30.19 Error: operator and operand don't agree [tycon
mismatch]
operator domain: 'Z -> 'Y -> 'Y
operand: bool
((XOR F) T) true
- val NOT = fn x => x F T;
val NOT = fn : (('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e) -> 'e

This shows the type of not, its argument needs to be of type
('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e
(it needs to be something that can accept F as first argument and T as
second argument).
This means that in XOR the type of the second input (since it is used
as an input for NOT) is also
('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e

So now in
XOR F T = F (NOT T) T = T
the type of this true is forced to be essentially
('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e

the type bool does not match with these input types.

Best,
Bart
Post by Fernando
F F T true false produces the expected answer. Why does it happen?
All the best,
Fernando
Fernando
2010-09-12 16:52:38 UTC
Permalink
Thank you very much, Bart, for the clear and nice explanation!

Warm regards,

Fernando
The basic difference is that the lambda calculus is not typed.  And
your example shows what happens with these definitions in a typed
context.
Best,
Bart
Continue reading on narkive:
Loading...