| I think we should "do the simplest thing that could possibly work", | and then see if we really need more. By "work", I mean a compatible | extension of H98 that makes it possible to add type signatures for | local bindings (which isn't always possible in H98). How about: | | * no implicit binding of type variables: to bind, use "forall". | | * pattern type annotations allowed only at the top level of pattern | bindings and lambda arguments (not on sub-patterns or arguments of | function bindings). | | * no result type annotations (except on pattern bindings, where they're | equivalent to top-level pattern type annotations). | I agree with the "simplest thing" plan. But if HPrime is to include existentials, we MUST have a way to name the type variables they bind, otherwise we can't write signatures that involve them. Stephanie and Dimitrios and I are working on this scheme: * Scoped type variables stand for type *variables*, not types. * Type variables are brought into scope only by one of two ways: a) The forall'd variables of a declaration type signature f :: forall a b. <type> f x y = e b) A pattern type signature may bring into scope a skolem bound in the same pattern: data T where MkT :: a -> (a->Int) -> T f (MkT (x::a) f) = ... The skolem bound by MkT can be bound *only* in the patterns that are the arguments to MkT (i.e. pretty much right away). The idea is that scoped type variables can be bound either at, or very close to, the point at which they are actually abstracted. This is a good topic to debate. S+D+I will try to put forth a set of rules shortly. Simon
On Wed, Feb 08, 2006 at 11:19:41AM -0000, Simon Peyton-Jones wrote:
I agree with the "simplest thing" plan. But if HPrime is to include existentials, we MUST have a way to name the type variables they bind, otherwise we can't write signatures that involve them. Stephanie and Dimitrios and I are working on this scheme: [...] b) A pattern type signature may bring into scope a skolem bound in the same pattern: data T where MkT :: a -> (a->Int) -> T f (MkT (x::a) f) = ...
The skolem bound by MkT can be bound *only* in the patterns that are the arguments to MkT (i.e. pretty much right away).
I see -- my scheme was overly simple. But this too feels unsatisfactory. What if we want to give signatures for both arguments? Will the a's be the same?
Sorry, but I cannot resist to mention an alternative language construct to scoped type variables which gives you the same power of annotating any subexpression with type information. I did mention it in my ICFP 2001 paper on Compositional Explanations of Types as a side note. The nice property of this language construct is that all type variables scope only over a single type; you never have to look if the same type variable appears somewhere else far away in your program. The idea is that a type may contain part of a type environment (so actually it is no longer a type but a typing). This typ environment constructs the relation to other types. Instead of f :: forall a. [a] -> ... f xs = ... where g :: a -> [a] g x = x:xs you write f :: [a] -> ... f xs = ... where g :: (xs::[b]) => b -> [b] g x = x:xs So (xs::[b]) is this new type environment that is part of the type of g. Whether you want to write it similar to a class context, is a matter of taste. This extended type (typing) is the principal monomorphic typing for the function g. Every subexpression has a principal monomorphic typing and hence you can annotate any expression with a typing. Type variables always scope only over a typing. This system of typings works fine for the Hindley-Milner system and also for Haskell 98 classes. I have to admit that I never looked beyond; so I don't know which problems may crop up for rank-n, existentials etc. Ciao, Olaf
participants (3)
-
Olaf Chitil -
Ross Paterson -
Simon Peyton-Jones