[cap-talk] Haskell @inert-like construct

[Kevin Reid]

On Sep 2, 2008, at 14:29, Tyler Close wrote:

> Hi Kevin,
>
> I want to follow up on your point about the similarity between
> Haskell's untyped parameters and the @inert annotation. Where's the
> best place to start reading?

The term is 'parametricity', I believe.
( http://en.wikipedia.org/wiki/Parametricity is unfortunately bare.)

They're not exactly untyped; they're of a entirely as-yet-undetermined  
type.

Suppose we have a function which transforms arbitrary lists in some  
way; its type is, most generally:

   forall a. [a] -> [a]

This is a parametrically polymorphic type - 'a' is a type variable. In  
any particular use of the function, 'a' is bound to some specific type  
(e.g. [Integer] -> [Integer]) -- but the function's type is general,  
so it cannot mention any type-specific operations -- it wouldn't  
typecheck!

For example, the type of "map (+1)" (which increments every number in  
a list) is *not* [a] -> [a], but rather:

   forall a. Num a => [a] -> [a]

That is, the type variable 'a' is required to be some numeric type.  
Any function having this type must have been verified by the type- 
checker to not contain any operations other than those on lists-in- 
general and those defined by the Num type-class.


So Haskell's type system lets you establish arbitrary "do only this  
(possibly empty) subset of operations on these objects" conditions,  
which in an, uh, less-typed system would require wrapping and  
unwrapping the objects to be protected (which becomes especially  
difficult in the presence of complex data structures holding said  
objects).


I asked #haskell for recommendations:

[18:45] <ddarius> kpreid: These behaviours are related to the free  
theorems, so you could look up those as well.
[18:45] <Saizan_> kpreid: the "theorems for free" of wadler are based  
on parametricity like that
[18:45] <earthy> http://people.cs.uu.nl/andres/ST-05-2003.pdf are the  
slides of the talk I mentioned
[18:46] <earthy> but the illustration was in terms of kinder chocolate  
surprise eggs

-- 
Kevin Reid                            <http://homepage.mac.com/kpreid/>