[Haskell-cafe] Mechanics of type-level proxies through branding?

[Dave Neuer]

Hi.

I'm a Haskell newbie, and I've been reading Oleg's work about
lightweight dependent types in Haskell, and I've been trying to figure
out if I understand how branding works (warning bells already, I
know).

At http://okmij.org/ftp/Computation/lightweight-dependent-typing.html#Branding,
he states "A language with higher-rank types or existential type
quantification lets us introduce type proxies for the values. We can
associate a value with some type in such a way that type equality
entails value equality..."

Then, in the code for eliminating array bounds checking at
http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs, the
following example of branding is given:

>> brand:: (Ix i, Integral i) => Array i e
>>                   -> (forall s. (BArray s i e, BIndex s i, BIndex s i) -> w)
>>                   -> w -> w
>> brand (a::Array i e) k kempty =
>>     let (l,h) = bounds a
>>     in if l <= h then k ((BArray a)::BArray () i e, BIndex l, BIndex h)
>>     else kempty
> ...
>
> The function brand has a higher-rank type. It is the existential
> quantification of 's' as well as the absence of BArray constructor
> elsewhere guarantee that the same brand entails the same bounds.

I think I understand that the fact that the type variable 's' is
shared between BArray, and BIndex's type constructors in the type
annotation for "brand", that the array and indices share the same
brand.

I also think I understand that since 's' is existentially quantified
and a phantom type, it's unique and cannot ever be unified w/ any
other type?

Additionally, it seems that this is all only within the scope of the
continuation? That is, "type equality entails value equality" but not
"value equality entails type equality", e.g. if I call brand two times
with arrays of the same bounds, I'd get two different brands?

Finally, I'm confused why the unit type in the explicit type
expression at BArray's value constructor application doesn't foil the
branding, i.e. why it doesn't destroy the uniqueness/opaqueness of
's'?

Thanks for anyone who can explain this!

Dave