On Thu, Nov 30, 2006 at 12:23:41PM +0000, Simon Marlow wrote:
Is kind ! visible to the programmer? How? What are you allowed/not allowed to do with something of kind !?
Yes it is, jhc has a rather robust kind system, originally developed to allow arbitrary typesafe mixing of strict and lazy code internally, I have found it quite useful to make its full power available to the programmer. A PTS is a type system that is parameterized by a set of 'sorts' that make up the kinds and superkinds in the system, a set of axioms describing the relationship between the sorts, and a set of rules describing what lambda abstractions are allowed based on sort. the PTS (pure type system) that jhc implements has the following 6 sorts. (in PTS's, both kinds and superkinds are considered "sorts") (#) - the kind of unboxed tuples # - the kind of unboxed values ! - the kind of boxed strict values * - the kind of boxed lazy values ** - the superkind of all boxed values ## - the superkind of all unboxed values the meaning of 'lazy' is exactly _|_ :: t iff t::* the axioms are as follows (*::**, #::##, (#)::##, !::**) basically, what you would expect, splitting things up into boxed and unboxed values. the way rules work are that they describe what you can abstract from what and then what the result is. so (#,*,*) - you can have a function from an unboxed value to a lazy boxed value and that function itself is lazy and boxed. (from,to,what) means we can have (\x:::from -> i:::to):::what a where ::: means the type of the type, so x:::y <-> exists t . x :: t and t :: y so, we have all of functions from any of #,*,! to #,*,! are allowed, and the result is a lazy boxed value. as a shortcut I will represent this as (*#!,*#!,*) (actually 9 rules in one) now there are a couple interesting ones: (*#!,(#),*) - a function may return an unboxed tuple and that function is lazy and boxed and the novel: ((#),*#!(#),!) - a function taking an unboxed tuple is a _strict_ value that is a function, meaning the function itself cannot be _|_. so, given the above rules, we can express any combination of lazy and strict interaction in a typesafe way. including the distinction between strict and lazy functional values. and on to the rules allowing types: (**,*,*) -- this says we can have functions from boxed types to values, as in forall a . a -> a we do not have a rule of the form (##,?,?) because an unboxed type cannot be passed to a function in a generic way, as values in it have a unique run-time representation. and we have (**,**,**) functions from types to types, such as the list constructor ([] :: * -> *) (**,##,##) - functions from types to unboxed types, often used as phantom arguments such as the declaration data Array__ a :: # making Array__ :: * -> # now, a great thing about this is that it is a valid PTS! so I get proofs of completeness, soundness, and a variety of robust typechecking algorithms for free! yay! in haskell source itself, you can use all of these kinds, the inference algorithm will only infer simple kinds, as in * or * -> * (ones made up of *'s and arrows) so you must use kind annotations to bring about other ones. some useful examples data StrictList a :: ! = Cons a (StrictList a) | Nil making StrictList :: * -> ! since a strictlist is of kind !, it can never contain _|_ in it, but the list argument is of kind *, so the list is strict in its spine, but may contain lazy values. data World__ :: # declares an unboxed type World__ with no values and hence no runtime representation. there is even a mild form of kind polymorphism allowed, with the folowing subkinding going on: ? / \ ?? (#) /\ *? # / \ * ! note that ?, ??, and *? are not kinds themselves, but can be used in haskell source files to represent that something can take more than one kind. for instance, IO has type data World__ :: # newtype IO (a::??) = IO (World__ -> (# World__, a #)) meaning, an IO action may return any sort of value, boxed, unboxed, strict or lazy (but not an unboxed tuple) any instantiation of IO will choose a concrete kind though. the declaration declares a simple sort of 'kind scheme'. none of ?, ??, or *? exist in core. they are only placeholders used in the kind inference algorithm presented to the programmer. an experimental feature is the 'undo' monad, whose syntax looks like the do monad, but is actually restricted to IO and function arguments and return values are automatically pulled into unboxed tuples and back again. It is entirely possible I mihht have an 'unboxed' mode, where '!' is the default infered kind for everything and unboxed tuples are automatically inserted at the appropriate points. it would make a very nice strict language with the full power of haskell type classes and the type system with the ability to call back and forth to haskell nicely! A front end for a strict language would just never produce anything of kind *. my original motivation for adding the ! kind was purely motivated by the back end, the grin back end is great at numerics, but is absolutely horrible at updates, doing update in place because I don't want to introduce the concept of redirections I would have to check for. Things of kind '!' never need indirections, as they are already evaluated, so they can use a more efficient representation, still boxed, but the code can just look directly into it or pass arguments to it without having to worry about it possibly being an unevaluated thunk. I am having some fun in 'undo', my strict toy language... so many distractions along the way, all I wanted was a nice way to avoid thunk indirections :) John -- John Meacham - ⑆repetae.net⑆john⑈