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

[Derek Elkins]

On Sat, May 22, 2010 at 8:36 PM, Dave Neuer <dave.neuer at pobox.com> 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.