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
abstraction.
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
<interactive>:1:0:
Kind error: `forall a. a' is applied to too many type arguments
About syntax:
(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
:t id
id :: a -> a
:k Id
Id :: * -> *
And I think anonymous type-level abstraction should look like this:
id' = \x -> x
type Id' = \x -> x
:t id'
id' :: a -> a
:k Id'
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
Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
