CODEWITHSUNDEEP
functional-programmingsml
anon_swe
anon_swe

Reputation: 9345

Functional Programming: Equivalence and Evaluation to a Value

I'm reading some notes on SML and am a bit confused by one of the author's remarks. Let e ==> v indicate evaluation to a value and e ~ e' indicate that e is extensionally equivalent to e'

The author writes:

If e ~ e' (both of type t) and there is an SML value v of type t s.t. e ~ v, then there is an SML value v' (again of type t), s.t. e' ==> v' and v ~ v'.

Make sure you notice that (and understand why we did not say here that if e ~ e' and e ~ v then e' ==> v.

Why not?

Upvotes: 1

Views: 248

Answers (2)

Andreas Rossberg
Andreas Rossberg

Reputation: 36098

Because that would mean that both reduce to the same syntactic value. But extensional equality is not the same as syntactic equality. It means, roughly, that there is no way for a program to tell the values apart.

Note in particular that function expressions are values themselves. But different function values with different bodies may still be extensionally equal, because they compute the same result when applied to the same argument. Trivial example:

fun x => x

and

fun x => let y = x in y

are two values that are syntactically different but extensionally equal.

Upvotes: 2

Cactus
Cactus

Reputation: 27626

If you start with e and e' being values v and v' already, then the second statement would say

If v ~ v' and v ~ v, then v' ==> v

which can be simplified as

If v ~ v', then v' ==> v

which is the exact opposite of extensionality, since you can have e.g.

v = fn x => x + 0
v' = fn x => x

which are not the same value, but are extensionally equal.

Upvotes: 1

Related Questions