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