| | When you say there's a good theoretical foundation (typed lambda
| | calcului) I think you are imagining that when we say
| |
| | f (x::a) = e
| |
| | we are saying "There's a /\a as well as a \x::a in this definition".
|
| No, that's not what I'm thinking.
OK, let me try to give some type rules for what I have in mind.
In these rules, I'm going to have an environment, T, that binds
user type variables to types. (A "user type variable" is a type
variable that appears in the program text.)
There is still a conventional type environment, G (usually written
Greek Gamma), that associates user term variables with their
types.
I'll just deal with type variables in lambda patterns, like
\ (x::a) -> E
Here's the rule:
x_i = free-term-vars(pat)
a_i = free-type-vars(pat) \ T
(T, a_i=taua_i); (G, x_i:taux_i) |- pat : tau_1
(T, a_i=taua_i); (G, x_i:taux_i) |-- E : tau_2
-------------------------------------------------------
T;G |- \pat -> E : tau_1 -> tau_2
The a_i are the type variables brought into scope by the pattern;
namely the free type variable of the pattern which are not already
in scope (hence the \ T).
The T environment is extended by binding each user type variable
a_i to a type taua_i that is gotten out of thin air (as is common in
type
rules). This new T env is used when typechecking the pattern itself and
the body E.
The intereesting bit is how to typecheck patterns, and type inside them:
T;G |- pat : tau
T |- ty : tau
-----------------
T;G |- pat::ty : tau
That is, to typecheck the pattern (pat::ty), typecheck pat and typecheck
ty.
The judgement T |- ty : tau checks that the user type ty is well formed
with
type tau. The key rule of this judgement looks up a type variable in T:
-----------------
T |- a : T(a)
OK, that's it. The point is simply that the user type variables are
regarded
as the name of a type; the programmer doesn't specify just what that
type
is. The type rules just 'inline' the type wherever the name is used.
All this translates into completely unmodified System F.
| OK, so there are two questions
| a) does that answer the question about the techincal foundation
| b) is it a good design from a software engineering point of view
|
| I hope the answer to (a) is yes, but I realise that opinions may
| differ about (b).
This message is really just a second attempt at (a)
Simon
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell