dekker@gucis.sct.gu.edu.au (Tony Dekker) (04/19/91)
Some Semantic Problems in Miranda (Re-Posting)
----------------------------------------------
The intended semantics of Miranda is that pairing is surjective, ie
_|_ = (_|_,_|_) is the least element of type (A,B) and that _|_ = \x._|_ is the
least element of type A->B. Essentially, the semantics maps each type to
an ideal in a domain, or to a set of Lambda terms together with an equivalence
relation. For (A,B) we have a categorical product domain, or a set of Lambda
terms with Beta equality and p = (fst p,snd p). For A->B we have a function
space, or a set of Lambda terms with Beta equality and extensionality. These
imply the two conditions with _|_.
However, the operational semantics is based on mapping Miranda terms to the
untyped Lazy Lambda Calculus (or rather, combinatory logic, which is almost the
same thing) which distinguishes _|_ from (_|_,_|_) = \x.x _|_ _|_ and _|_ from
\x._|_.
The attempted solution is to define ALL operations on type (A,B) in terms of
fst and snd so that _|_ and (_|_,_|_) aren't distinguished. As a result,
f (x,y) = 3
really defines a constant function. SHOW functions also don't distinguish _|_
and (_|_,_|_). Function application doesn't distinguish _|_ from \x._|_ and
neither do SHOW functions (all functions print as <function>, without
exception).
The problem is that the "convergence-testing" primitive seq defined such that:
seq x y = _|_, x=_|_
= y, otherwise
distinguishes (_|_,_|_) from _|_ and \x._|_ from _|_. This primitive is
inter-definable with:
strict f x = _|_, x=_|_
= f x, otherwise
since strict f x = seq x (f x) and seq x y = strict (const y) x.
The function strict is necessary for synchronising input/output and for
defining foldl.
And this isn't easily fixed: if _|_ = (_|_,_|_) is the least element of type
(A,B) then eg:
strict (const x) (y,z) = x, y~=_|_ or z~=_|_
= _|_, y=z=_|_
which is an inherently parallel function! (It waits until one of y or z
terminates, and then kills the other one and returns x).
We can also distinguish _|_ from \x._|_ using polymorphic equality:
(\x._|_ = \x._|_) gives a runtime error while (_|_ = _|_) gives _|_. However,
we could solve this by banning equality on functions, eg by having the type of
equality involve special type variables which cannot be instantiated to arrow
types. Perhaps we could restrict the applicability of strict and seq similarly.
If we really want to pretend that _|_ = (_|_,_|_), ie product is categorical
(coalesced) product, and _|_ = \x._|_, ie equality is extensional, we must
define a convergence-testing construct for each type, just as there is a SHOW
function for each type:
seq x y = if x = x then y else b
num where
b = b
seq [] y = y
[A]
seq (h:t) y = y
[A]
seq (InL x) y = y
A+B
seq (InR x) y = y
A+B
seq x y = if por (seq (fst x) True) (seq (snd x) True) then y else b
(A,B) A B
where
b = b
Here por is "parallel or". Plotkin in his classical paper on PCF and full
abstraction defines two inherently parallel operations:
pcond :: bool -> * -> * -> *
pcond x y z = y, x = True || this condition is a semantic one
= z, x = False || not Miranda code
= y, x = _|_ and y = z
exists :: (nat -> bool) -> bool
exists f = False, f _|_ = False
= True, f 0 = True or f 1 = True or ...
The idea is (exists f) approximates the predicate calculus statement E x.f x
Using these operations,
por x y = pcond x True y
We can also define a version of seq for functions, at least those defined
on nat. If
f :: nat -> A
we define
f' :: nat -> bool
f' n = seq (f n) True
A
seq f x = if exists f' then x else b
nat->A
where
b = b
So the question of convergence-testing is completely tied up with the question
of full abstraction, somehow.
The questions I'd like to ask are:
- What do we really intend strictness on pairs and functions to mean?
- Can we implement what we intend?
- What use are such functions?
- Does HASKELL have these problems?
- Is this an argument for adding por to Miranda?
- What exactly is the relationship between convergence-testing and full
abstraction?
- How does this affect strictness analysis?
For example, \f.\x.f x is strict on f
\x.(x,x) is strict on x
\x.(x,_|_) is strict on x
\x.(x,3) is NOT strict on x
\(x,y).x = fst is strict on (x,y)
Clearly \x.(M,N) is strict on x if \x.M and \x.N are both strict on x.
Any ideas anyone?
Tony Dekker