Hi all,

On Wed, Nov 12, 2008 at 2:09 PM, Lennart Augustsson <lennart@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