darcs-2.18.3: a distributed, interactive, smart revision control system
Safe HaskellSafe-Inferred
LanguageHaskell2010

Darcs.Patch.Witnesses.Sealed

Synopsis

Documentation

data Sealed a where Source #

A Sealed type is a way of hide an existentially quantified type parameter, in this case wX, inside the type. Note that the only thing we can currently recover about the existentially quantified type wX is that it exists.

Constructors

Sealed :: a wX -> Sealed a 

Instances

Instances details
Show1 a => Show (Sealed a) Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

showsPrec :: Int -> Sealed a -> ShowS #

show :: Sealed a -> String #

showList :: [Sealed a] -> ShowS #

Eq2 a => Eq (Sealed (a wX)) Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

(==) :: Sealed (a wX) -> Sealed (a wX) -> Bool #

(/=) :: Sealed (a wX) -> Sealed (a wX) -> Bool #

seal :: a wX -> Sealed a Source #

data Sealed2 a where Source #

The same as Sealed but for two parameters (wX and wY).

Constructors

Sealed2 :: !(a wX wY) -> Sealed2 a 

Instances

Instances details
Show2 a => Show (Sealed2 a) Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

showsPrec :: Int -> Sealed2 a -> ShowS #

show :: Sealed2 a -> String #

showList :: [Sealed2 a] -> ShowS #

seal2 :: a wX wY -> Sealed2 a Source #

data FlippedSeal a wY where Source #

Constructors

FlippedSeal :: !(a wX wY) -> FlippedSeal a wY 

flipSeal :: a wX wY -> FlippedSeal a wY Source #

unseal :: (forall wX. a wX -> b) -> Sealed a -> b Source #

mapSeal :: (forall wX. a wX -> b wX) -> Sealed a -> Sealed b Source #

mapFlipped :: (forall wX. a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ Source #

unseal2 :: (forall wX wY. a wX wY -> b) -> Sealed2 a -> b Source #

mapSeal2 :: (forall wX wY. a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b Source #

unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b Source #

data Dup p wX wY where Source #

Duplicate a single witness. This is for situations where a patch-like type is expected, i.e. a type with two witnesses, but we have only a type with one witness. Naturally, any concrete value must have both witnesses agreeing.

Note that Sealed (Dup p wX) is isomorphic to p wX.

Constructors

Dup :: p wX -> Dup p wX wX 

data FreeLeft p Source #

FreeLeft p is forall x . exists y . p x y In other words the caller is free to specify the left witness, and then the right witness is an existential. Note that the order of the type constructors is important for ensuring that y is dependent on the x that is supplied. This is why Stepped is needed, rather than writing the more obvious Sealed (Poly p) which would notionally have the same quantification of the type witnesses.

Instances

Instances details
Gap FreeLeft Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

emptyGap :: (forall wX. p wX wX) -> FreeLeft p Source #

freeGap :: (forall wX wY. p wX wY) -> FreeLeft p Source #

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> FreeLeft p -> FreeLeft q -> FreeLeft r Source #

data FreeRight p Source #

FreeRight p is forall y . exists x . p x y In other words the caller is free to specify the right witness, and then the left witness is an existential. Note that the order of the type constructors is important for ensuring that x is dependent on the y that is supplied.

Instances

Instances details
Gap FreeRight Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

emptyGap :: (forall wX. p wX wX) -> FreeRight p Source #

freeGap :: (forall wX wY. p wX wY) -> FreeRight p Source #

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> FreeRight p -> FreeRight q -> FreeRight r Source #

unFreeLeft :: FreeLeft p -> Sealed (p wX) Source #

Unwrap a FreeLeft value

unFreeRight :: FreeRight p -> FlippedSeal p wX Source #

Unwrap a FreeRight value

class Gap w where Source #

Gap abstracts over FreeLeft and FreeRight for code constructing these values

Methods

emptyGap :: (forall wX. p wX wX) -> w p Source #

An empty Gap, e.g. NilFL or NilRL

freeGap :: (forall wX wY. p wX wY) -> w p Source #

A Gap constructed from a completely polymorphic value, for example the constructors for primitive patches

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> w p -> w q -> w r Source #

Compose two Gap values together in series, e.g. 'joinGap (+>+)' or 'joinGap (:>:)'

Instances

Instances details
Gap FreeLeft Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

emptyGap :: (forall wX. p wX wX) -> FreeLeft p Source #

freeGap :: (forall wX wY. p wX wY) -> FreeLeft p Source #

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> FreeLeft p -> FreeLeft q -> FreeLeft r Source #

Gap FreeRight Source # 
Instance details

Defined in Darcs.Patch.Witnesses.Sealed

Methods

emptyGap :: (forall wX. p wX wX) -> FreeRight p Source #

freeGap :: (forall wX wY. p wX wY) -> FreeRight p Source #

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> FreeRight p -> FreeRight q -> FreeRight r Source #