proposal: add 'unsafeCoerce'

[John Meacham]

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⑈