16 Jan
2007
16 Jan
'07
8:01 a.m.
On 1/16/07, Chung-chieh Shan
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@s), which in retrospect seems greedy. :-) Thanks, Jim