On Sat, May 22, 2010 at 8:36 PM, Dave Neuer wrote:

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.

First, Haskell lacks (free) existential type quantifiers, so the above uses universal quantification. The usage is equivalent to using an existential but it is an encoding and so it is important to know what is being encoded or alternatively to stick just to the actual universal quantification that is there. Second, this function encodes more than is necessary. It is necessary to use a CPS style for the encoding of existentials, but the above code also CPS encodes a case analysis. Here's an equivalent implementation and a proof that it is equivalent. Here and elsewhere I'll set i to Int for simplicity. {-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-} import Data.Array newtype BA s e = BArray (A e) newtype BI s = BIndex Int type A e = Array Int e brand :: A e -> (forall s. (BA s e, BI s, BI s) -> w) -> w -> w brand (a :: A e) k kempty = let (l,h) = bounds a in if l <= h then k (BArray a :: BA () e, BIndex l, BIndex h) else kempty brand' :: A e -> (forall s. Maybe (BA s e, BI s, BI s) -> w) -> w brand' (a :: A e) k = k (if l <= h then Just (BArray a :: BA () e, BIndex l, BIndex h) else Nothing) where (l,h) = bounds a brandFromBrand' :: A e -> (forall s. (BA s e, BI s, BI s) -> w) -> w -> w brandFromBrand' a k kempty = brand' a (maybe kempty k) brand'FromBrand :: A e -> (forall s. Maybe (BA s e, BI s, BI s) -> w) -> w brand'FromBrand a k = brand a (k . Just) (k Nothing) Once you see the Maybe it's easier to see what the existential type would be if Haskell had the appropriate existentials. brand :: A e -> exists s. Maybe (BA s e, BI s, BI s) or equivalently brand :: A e -> Maybe (exist s. (BA s e, BI s, BI s)) Using local existential quantification which GHC supports we can encode the above and prove it equal to the earlier representations. data B e = forall s. B (BA s e) (BI s) (BI s) brand'' :: A e -> Maybe (B e) brand'' a = if l <= h then Just (B (BArray a) (BIndex l) (BIndex h)) else Nothing where (l,h) = bounds a brand''FromBrand' :: A e -> Maybe (B e) brand''FromBrand' a = brand' a (fmap (\(ba,l,h) -> B ba l h)) brand'FromBrand'' :: A e -> (forall s. Maybe (BA s e, BI s, BI s) -> w) -> w brand'FromBrand'' a k = case brand'' a of Nothing -> k Nothing Just (B ba l h) -> k (Just (ba, l, h))

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.

Correct.

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?

The phantom type aspect is irrelevant. s is a phantom type because we don't need to actually represent it in any way. As far as the rest of the paragraph it's somewhat tricky though I think you've got the right idea. Whether s can unify with something depends on your perspective. In general, when introducing a universal quantifier we need to treat the quantified variable as a fresh constant that doesn't unify with anything. This guarantees that we aren't making any assumptions about it. When eliminating a universal quantifier, we do allow unification, or, when instantiation is explicit, we explicitly are saying what type to unify the type variable with. The rules for existentials are dual. brand is eliminating a universal and brand'' is equivalently introducing an existential, within the body of brand/brand'' so s can and does unify. In brand it is unified with (). Consumers of these will be doing the dual operation and so they must not unify s.

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?

Yes. The existential forgets what the quantified type was completely so it has no way of comparing the two types to see if they are equal. The existential in OO classes does the same thing and is what leads to the "binary method problem." At any rate, the brands are completely independent of the bounds, the connection is one of convention in the same way that within a Set abstract data type implemented with lists that the list represents a set is a convention.

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'?

We only allow consumers that guarantee that they don't "look" at s. At that point it doesn't matter what we set s to.