Hello all,
When I was recently thinking about an attribute grammar extension of
Haskell -- maybe more on that later -- I came upon the subject of
types and type synonyms, and from there on to coercions. Since I am
certainly no expert on typechecking, maybe someone else can help me
out on this.
In the Haskell Report 1.3 it says
"Type synonyms are a strictly syntactic mechanism to make type
signatures more readable. A synonym and its definition are
completely interchangable."
(BTW, these sentences are the first of section 4.2.3, but they
probably should be the last of the previous section.) This is
against my intuition. I would say that a type synonym introduces
a new type, of which the programmer knows nothing except that there
exists a way to convert the synonym and its definition to each
other. Thus, String is different from [Char], but
"some string" -- is of type String
"another string" :: [Char] -- is of type [Char]
['c','h','a','r'] -- is of type [Char]
['R','i','k','a'] :: String -- is of type String
In this case the coercion is performed by an explicit type
annotation. For datatypes not defined using type synonyms the
programmer might provide a coercion. In that case, the declaration
coercion intToReal :: Int -> Real
would cause the following equality to hold:
42 :: Real = intToReal 42
Here a type annotation is used to coerce the Int value 42 to the
corresponding Real value. It is not always necessary to make this
coercion explicit, since it can be inserted automatically using
available type information. As an example, given
sin :: Real -> Real
together with the above coercion, we have this equality:
sin 5 = sin (intToReal 5)
To conclude I propose the following:
(1) a `type' declaration introduces a new type + two anonymous
coercions;
(2) coercions can also explicitly be provided using `coercion'
declarations;
(3) a type annotation forces the annotated expression to be of the
given type, if necessary after the application of a coercion
function (this is _explicit_ coercion);
(4) if an expression is of type A when type B is expected, and a
coercion function is defined of type A -> B, then it is
automatically inserted (this is _implicit_ coercion);
I think that (1) and (4) together give an interpretation of type
synonyms that works the same in practice as the current Haskell view
that was cited above. (4) together with the generalisation to
programmer-defined coercion functions per (2) may replace the
`fromInteger' rule in Haskell, by taking all integer literals to be
of type Int and declaring
coercion fromInteger :: Num a => Int -> a
Finally (3) is a straight generalization of the current use of type
annotations in expressions; I suspect that such annotations can be
used instead of the constructor introduced by a `newtype'
declaration.
Of course there are still a few problems, such as the type of
["what is", "my type?" :: [Char]]
which could be either String or [Char], and the treatment of
polymorphic types and type classes. But these can probably be
worked out.
Does the above make any sense?
Groetjes,
<><
Marnix
--
Marnix Klooster
[EMAIL PROTECTED] // [EMAIL PROTECTED]
