[Haskell-cafe] Proof that Haskell is RT

[Benja Fallenstein]

Hi all,

On Wed, Nov 12, 2008 at 2:09 PM, Lennart Augustsson
<lennart at augustsson.net>wrote:

> You can't write a straightforward dynamic semantics (in, say,
> denotational style) for Haskell.
> The problem is that with type classes you need to know the types
> compute the values.

...

> It's possible that there's some more direct approach that represents
> types as some kind of runtime values, but nobody (to my knowledge) has
> done that.


It seems to me that if you don't need your semantics to do the work of
type-*checking* (i.e., you don't care if the rules assign some strange
denotation to an ill-typed term), there is a natural approach to giving
semantics to 98-style type classes. I'm figuring out the details as I type,
though; if anybody sees anything that does not work, please do tell!

Let "type" mean a non-overloaded type expression (i.e., not containing
variables). I'll suppose that you already know the set of types in the
program and the domain associated with each type. (This is usual in
denotational treatments, right?) Let the domains be such that all sets of
elements have a join (i.e., complete lattices). Define the domain of
"overloaded values" to be the domain of functions from types to values of
these types or "bottom" (when I say "bottom" in the following, it is this
bottom, which is below the domain's bottom), i.e., the product of the
liftings of the domains of all possible types. The interpretation of
"bottom" is, "this overloaded value doesn't have an instance at this type"
(e.g., [7,9] is "bottom" at type Bool).

An *environment* is a function from symbols to overloaded values. The
denotation of an expression is a function from environments to overloaded
values; the denotation of a definition list is a function from environments
to environments; the denotation of a whole program is the least fixed point
of the definition list that makes up the program.

Expressions are interpreted as follows (update :: Symbol -> OverloadedValue
-> Environment -> Environment is defined in the natural way):

[[x]] = \env type. env "x" type
[[T :: TYPE]] = \env type. if type instance of TYPE then [[T]] env type else
bottom
[[F X]] = Join_type2. \env type1. [[F]] env (type1 -> type2) $ [[X]] env
type2
[[\x. T]] = \env type. case type of
    (type1 -> type2) -> \val. [[T]] (update "x" (mono type1 val) env) type2
    otherwise -> bottom
  where mono ty val = \ty'. if ty == ty' then val else bottom
[[let x=S in T]] = \env type.
    [[T]] (fix $ \env'. update "x" ([[S]] env') env) type

Simple definitions are interpreted in the obvious way:

[[x = T]] = \env sym. if sym == "x" then ([[T]] env) else (env sym)
[[x :: Ty; x = T]] = [[x = T :: Ty]]

Finally, instance declarations are interpreted in a special way. To
interpret the declaration

    instance C Ty1 .. Tyn where
        ...; xi = Ti; ...

we need to know the set of possible types for xi. (No type inference should
be necessary -- the class declaration + the Ty1 .. Tyn from the instance
declaration should give us all the necessary information, right?) Call this
set Types. Then,

[[xi = Ti]] = \env sym type. if sym == "xi" && type in Types then [[T]] env
type else env sym type

That is, an instance declaration sets the value of a symbol at some types,
and leaves the values at the other types alone.

Some notes:

* If T is a well-typed term and type is *not* a type instance of that term,
then ([[T]] env type) is bottom.

* In particular, [[T :: TYPE]] env type = [[T]] env type, when type is an
instance of TYPE; otherwise, [[T :: TYPE]] env type = bottom.

* Application is supposed to be strict in "bottom": bottom x = bottom; f
bottom = bottom.

* In interpreting [[F X]], we take the join over all possible types of X
("type2"). If X is monomorphic, then ([[X]] env type2) is bottom for all
types except the correct one, so the join gives the correct denotation. If X
is polymorphic, but the type of F together with the type forced by the
context of (F X) together determine what type of X must be used, then either
([[F]] env (type1 -> type2)) or ([[X]] env type2) will be bottom for every
type2 exept for the one we want to use; so the application ([[F]] ... $
[[X]] ...) will be bottom except for the correct type; so again, the join
will give the correct denotation. (Caveat lector: I haven't proved this, I'm
running on intuition :))

* In the interpretation of expressions like (show (read "5")), the join is
non-degenerate: it consists of the join of "5", "5.0" etc. But since such
expressions are rejected by the type-checker, we don't care.

* Lets containing multiple definitions can be translated as in the Haskell
report, if we add an interpretation for a case construct (I'm too lazy to
try):
http://www.haskell.org/onlinereport/exps.html#sect3.12

* In the interpretation of the lambda expression, we need to interpret the
body of the expression separately for every type of the lambda expression;
the function 'mono' converts the monomorphic parameter value into an
OverloadedValue that is bottom everywhere except at the monomorphic type. In
the interpretation of 'let', and of top-level definitions, on the other
hand, we don't have 'mono' -- we update the environment with an
OverloadedValue. I was surprised to have the "lambda arguments are
monomorphic" rule from the Hindley-Milner system forced upon me like that!
:-)

* Neil's example, (show (f [])) where either f = id :: [Int] -> [Int] or f =
id :: [Char] -> [Char], is taken care of straight-forwardly. The
interpretation of f = (id :: [Int] -> [Int]]) is bottom at all types except
[Int] -> [Int]; therefore, (f []) is bottom at all types except [Int];
therefore, in the join over all possible types in the application (show (f
[])), only the type ([Int] -> String) of show is actually used.


Comments? Problems? [ I hope *somebody* is actually going to read this mail
-- I don't have the time to make it less confusing, sorry :-( ]

Thanks,
- Benja
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081112/19dead3b/attachment.htm