[Haskell-cafe] lifting restrictions on defining instances
rendel at cs.au.dk
Tue Jul 28 08:28:05 EDT 2009
wren ng thornton wrote:
>>> Thus, the forall keyword is serving as the type-level abstraction.
>> What do you mean by "type-level abstraction" here?
> I mean an abstraction, as in a lambda-abstraction (aka a
> lambda-expression), at the type level.
> I'm not sure I follow what you mean.
I mean that the forall keyword is *not* serving as the type-level
There is a difference between abstraction (as in lambda abstraction) and
the type of abstractions (as in function types). In pure type systems,
we have two different binders for these different features:
- lower-case lambda for abstraction (on all levels)
- upper-case Pi for the type of abstractions (on all levels)
I find it highly confusing to say that forall denotes type-level
abstraction, because it does not denote abstraction at all. It rather
denotes the type of an abstraction, namely in Haskell, the type of
abstracting over types in terms.
In other words, the following is not legal Haskell, and not how forall
works in any polymorphic lambda calculus:
> -- Just a type-level lambda
> five :: (forall a. a) Int
> five = 5
> -- Making the term-level match the type exactly
> five :: (forall a. a) Int
> five = (/\a. 5::a) @Int
Note that (forall a . a) has kind *, so (forall a . a) Int is not even
well-kinded, as ghci correctly determines:
> ghci -XRankNTypes
> :k (forall a. a)
(forall a. a) :: *
> :k (forall a . a) Int
Kind error: `forall a. a' is applied to too many type arguments
>> (1) abstraction over terms in terms (to construct functions)
>> (2) abstraction over types in terms (to construct polymorphic values)
>> (3) abstraction over types in types (to construct type functions)
> The syntax of #3 could also be conflated with the syntax of #2, for
> the same reason: they are in different syntactic categories. I
> pointed this out because the capital-lambda was the syntax others in
> the thread were using. Also, it makes sense to me to have #2 and #3
> ("abstraction over types in _") paired together, rather than #1 and
> #3 ("abstraction over X in X"). Pairing #2/#3 also gives term/type
> symmetry as we have for other built-ins like , (,), and -> (though
> the symmetry is imperfect for ->).
I agree that this makes as much sense as my view.
However, I still argue that the existing type/kind symmetry for ->
should be reflected in a term/type symmetry for \. We already have:
id x = x
type Id x = x
id :: a -> a
Id :: * -> *
And I think anonymous type-level abstraction should look like this:
id' = \x -> x
type Id' = \x -> x
id' :: a -> a
Id' :: * -> *
I would use the upper-case lambda for kind-polymorphism on the type level.
type Id'' = /\k -> \t :: k -> t
:k Id'' :: forall k . k -> k
:k Id'' [*] :: * -> *
:k Id'' [*] Int = Int
:k Id'' [forall k . k -> k] Id'' [*] Int = Int
More information about the Haskell-Cafe