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
