patch applied (haskell-prime-status): accept scoped type variables
Mon Apr 14 12:05:50 PDT 2008 Simon Marlow [EMAIL PROTECTED] * accept scoped type variables M ./status.hs -1 +1 View patch online: http://darcs.haskell.org/haskell-prime-status/_darcs/patches/20080414190550-8214f-d308ff4f7fc7ca2c58b885792e45ab33c2735e77.gz ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Capitalized type variables (was Re: Scoped type variables)
I wrote: What I don't like is that given a signature like x :: a - a there's no way to tell, looking at it in isolation, whether a is free or bound in the type. [...] Here's a completely different idea for solving this. It occurs to me that there isn't all that much difference between capitalized and lowercase identifiers in the type language. One set is for type constants and the other for type variables, but one man's variable is another man's constant, as the epigram goes. In Haskell 98 type signatures, the difference between them is precisely that type variables are bound within the type, and type constants are bound in the environment. Maybe scoped type variables should be capitalized. At the usage point this definitely makes sense: you really shouldn't care whether the thing you're pulling in from the environment was bound at the top level or in a nested scope. And implicit quantification does the right thing. As for binding, I suppose the simplest solution would be explicit quantification of the capitalized variables, e.g. f :: forall N. [N] - ... f x = ... or f (x :: exists N. [N]) = ... Really, the latter binding should be in the pattern, not in the type signature, but that's trickier (from a purely syntactic standpoint). What do people think of this? I've never seen anyone suggest capitalized type variables before, but it seems to make sense. -- Ben ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Scoped type variables
On Wed, Feb 08, 2006 at 05:48:24PM -, Simon Peyton-Jones wrote: | 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). [...] f (MkT (x::a) (f::a-Int)) = ... You can imagine that either (a) both bind 'a' to the skolem, but must do consistently; or (b) that (x::a) binds 'a', and (f::a-Int) is a bound occurrence. It doesn't matter which you choose, I think. Another possibility would be to allow an optional explicit quantifier before the data constructor, mirroring the old datatype syntax for existentials: data T = forall a. MkT a (a-Int) f (forall a. MkT x f) = ... ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Scoped type variables
On Tue, Feb 07, 2006 at 08:15:19PM +, Ben Rudiak-Gould wrote: Simon PJ thinks that Haskell' should include scoped type variables, and I tend to agree. But I'm unhappy with one aspect of the way they're implemented in GHC. What I don't like is that given a signature like x :: a - a there's no way to tell, looking at it in isolation, whether a is free or bound in the type. A second problem with GHC's provision of scoped type variables is the confusing variety of ways of doing it. Some of them address the same problem that partial type signatures aim at (e.g. by allowing signatures for parts of arguments and/or the result of functions). Partial type signatures may well not be ready in time for Haskell', but we should still try to avoid overlap. 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). ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
RE: Scoped type variables
| 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Scoped type variables
Simon PJ thinks that Haskell' should include scoped type variables, and I tend to agree. But I'm unhappy with one aspect of the way they're implemented in GHC. What I don't like is that given a signature like x :: a - a there's no way to tell, looking at it in isolation, whether a is free or bound in the type. Even looking at the context it can be hard to tell, because GHC's scoping rules for type variables are fairly complicated and subject to change. This situation never arises in the expression language or in Haskell 98's type language, and I don't think it should arise in Haskell at all. What I'd like to propose is that if Haskell' adopts scoped type variables, they work this way instead: 1. Implicit forall-quantification happens if and only if the type does not begin with an explicit forall. GHC almost follows this rule, except that forall. (with no variables listed) doesn't suppress implicit quantification---but Simon informs me that this is a bug that will be fixed. 2. Implicit quantification quantifies over all free variables in the type, thus closing it. GHC's current behavior is to quantify over a type variable iff there isn't a type variable with that name in scope. Some care is needed in the case of class method signatures: (return :: a - m a) is the same as (return :: forall a. a - m a) but not the same as (return :: forall a m. a - m a). On the other hand the practical type of return as a top-level function is (Monad m = a - m a), which is the same as (forall m a. Monad m = a - m a), so this isn't quite an exception depending on how you look at it. I suppose it is a counterexample to my claim that Haskell 98's type language doesn't confuse free and bound variables, though. If rule 2 were accepted into Haskell' and/or GHC, then code which uses implicit quantification and GHC scoped type variables in the same type would have to be changed to explicitly quantify those types; other programs (including all valid Haskell 98 programs) would continue to work unchanged. Note that the signature x :: a, where a refers to a scoped type variable, would have to be changed to x :: forall. a, which is potentially confusable with x :: forall a. a; maybe the syntax forall _. a should be introduced to make this clearer. The cleanest solution would be to abandon implicit quantification, but I don't suppose anyone would go for that. With these two rules in effect, there's a pretty good case for adopting rule 3: 3. Every type signature brings all its bound type variables into scope. Currently GHC has fairly complicated rules regarding what gets placed into scope: e.g. f :: [a] - [a] f = ... brings nothing into scope, f :: forall a. [a] - [a] f = ... brings a into scope, f :: forall a. [a] - [a] (f,g) = ... brings nothing into scope (for reasons explained in [1]), and f :: forall a. (forall b. b - b) - a f = ... brings a but not b into scope. Of course, b doesn't correspond to any type that's accessible in its lexical scope, but that doesn't matter; it's probably better that attempting to use b fail with a not available here error message than that it fail with a no such type variable message, or succeed and pull in another b from an enclosing scope. There are some interesting corner cases. For example, rank-3 types: f :: ((forall a. a - X) - Y) - Z f g = g (\x - exp) should a denote x's type within exp? It's a bit strange if it does, since the internal System F type variable that a refers to isn't bound in the same place as a itself. It's also a bit strange if it doesn't, since the identification is unambiguous. What about shadowing within a type: f :: forall a. (forall a. a - a) - a I can't see any reason to allow such expressions in the first place. What about type synonyms with bound variables? Probably they should be alpha-renamed into something inaccessible. It seems too confusing to bring them into scope, especially since they may belong to another module and this would introduce a new notion of exporting type variables. I like rule 3 because of its simplicity, but a rule that, say, brought only rank-1 explicitly quantified type variables into scope would probably be good enough. Rules 1 and 2 seem more important. I feel like a new language standard should specify something cleaner and more orthogonal than GHC's current system. -- Ben [1]http://www.mail-archive.com/glasgow-haskell-users@haskell.org/msg09117.html ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Scoped type variables
Ben Rudiak-Gould wrote: Simon PJ thinks that Haskell' should include scoped type variables, and I tend to agree. But I'm unhappy with one aspect of the way they're implemented in GHC. What I don't like is that given a signature like x :: a - a there's no way to tell, looking at it in isolation, whether a is free or bound in the type. I'd quite like to see a flag that switches off implicit forall quantification altogether, or maybe just warned about it (since I use -Wall -Werror anyway). id :: forall a. a - a const :: forall a b. a - b - a etc. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
scoped type variables in class instances
The Haskell Prime Wiki mentions the scoping of type variables in class instances, but only as an aside, and it is not even clear whether proposal 1 would support that feature or not. For me this once occurred as a matter of language expressiveness, i.e. I had once to switch from hugs to GHC, because I could not find a way of expressing in Hugs what I needed. The problematic piece of code was the following: instance (LUB a b c,Full c d) = Run(a-b) where interpret e a = (p1.p2)(evalExp [(e2.e1) a] (expand e)) where e1 = embed :: a-c e2 = embed :: c-d p2 = project :: d-c p1 = project :: c-b As you can see, this is using multi-parameter classes (and functional dependencies), and whether it is a matter of language expressiveness or not is probably connected to whether these features are around or not. Explanation: An instance Run t meant to provide an evaluation of expressions (some fixed type) that returns type t. This essentially worked by picking one of the approximants of the D_infty model that was big enough to do the evaluation in, embed inputs into that type, evaluate over there, and then project results out of it. The class instance above is the case for function types. To do this for a-b, I first need to find an upper bound into which I can safely embed/project types a and b - and that is c; then I find the next type into which I can embed c, at which I can do D_infty-style evaluation, and that is d. I get these types from deterministic multi-parameter classes. The embed/project functions come from the class instances LUB a b c and Full c d. There are instances giving me versions of embed with the same argument type but different result types, thus I need to be able to tell my program which ones to use when they are applied to a value of type a. Above, I do this with type annotations, but I need that the type variables I use here correspond to those of the class instance definition. In hugs, I was stumped. Stefan Kahrs ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
