On 4/16/12 7:49 PM, Jonathan S. Shapiro wrote:
> This is an idea that I never got around to implementing, but I sort of
> think is important. It's also pretty half-baked.
Just in case you haven't realized it yet, what you want is essentially the
difference between rank-1 and rank-2 quantifiers. Looking at things
through the other side of the lens, when I say:
foo : forall a b. (a -> b) -> b
I'm saying that given any particular choice of A and B, I can transform
(A->B) into B. For this particular example, the only implementation
options are to go into an infinite loop, or to pass an undefined value to
the function argument and hope it doesn't explode.
However, when I say:
bar : forall b. (forall a. a -> b) -> b
I'm saying that given any particular choice of B, I can transform (forall
a. a -> B) into B. That is, I require that the function argument be
polymorphic in a: the function you give me must be good for any particular
type I please. In this case, a viable implementation is to have a
particular A in mind and a particular value of A on hand, and then I'll
pass that value and type to whatever function you give me.
Another example which perhaps hits closer to home is the distinction
between (type-level) "parameters" and "arguments" in dependently typed
languages. That is, when I give the definition:
data Vec a : Nat -> Type where
Nil : Vec a 0
Cons : a -> Vec a n -> Vec a (n+1)
The first and second argument to Vec behave differently. The first
argument is parametric because it's fixed for all the constructors and
therefore the constructors are natural in that argument. The second
argument is non-parametric because there's an interplay between the
particular argument/constructor pairs we're allowed to use.
TL;DR: this sort of thing has been studied extensively. Your example is a
bit more like the dependent type example since it doesn't conflate the
parametricity component with the depth of nesting into contravariant
positions; but both perspectives may offer insight into how to do it.
--
Live well,
~wren
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
