[Haskell-cafe] Re: Higher kinds (and impredicativity?)

[Jim Apple]

On 1/16/07, Chung-chieh Shan <ccshan at post.harvard.edu> wrote:
> in particular, if a type is well-kinded (i.e., well-formed)
> then it should either be a "value type" (such as "[Int]" and "forall a.
> a") or contain a redex (such as "(\a -> a) Int").

I think I see. I was expecting that (forall v : k . t)@s could
beta-reduce to (forall v : k . t at s), which in retrospect seems greedy.
:-)

Thanks,
Jim