Safe Haskell	None
Language	Haskell2010

Data.Array.Nested.Types

Contents

Reasoning helpers
Reified evidence of a type class
Type-level naturals
Type-level lists
Unsafe

Synopsis

subst1 :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). (a :~: b) -> f a :~: f b
subst2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (c :: k2) (a :: k1) (b :: k1). (a :~: b) -> f a c :~: f b c
data Dict (c :: k -> Constraint) (a :: k) where
- Dict :: forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
pattern SZ :: () => n ~ 0 => SNat n
pattern SS :: forall np1 n. () => (n + 1) ~ np1 => SNat n -> SNat np1
fromSNat' :: forall (n :: Nat). SNat n -> Int
sameNat' :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m)
snatPlus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
snatMinus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
snatMul :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
snatSucc :: forall (n :: Nat). SNat n -> SNat (n + 1)
type family (l1 :: [a]) ++ (l2 :: [a]) :: [a] where ...
type family Replicate (n :: Natural) (a1 :: a) :: [a] where ...
lemReplicateSucc :: forall {a1} (a2 :: a1) (n :: Natural). (a2 ': Replicate n a2) :~: Replicate (n + 1) a2
type family MapJust (l :: [a]) = (r :: [Maybe a]) | r -> a l where ...
lemMapJustEmpty :: forall {a} (sh :: [a]). (MapJust sh :~: ('[] :: [Maybe a])) -> sh :~: ('[] :: [a])
lemMapJustCons :: forall {a} (sh :: [a]) (n :: a) (sh' :: [Maybe a]). (MapJust sh :~: ('Just n ': sh')) -> sh :~: (n ': Tail sh)
type family Head (l :: [k]) :: k where ...
type family Tail (l :: [a]) :: [a] where ...
type family Init (l :: [a]) :: [a] where ...
type family Last (l :: [k]) :: k where ...
unsafeCoerceRefl :: forall {k} (a :: k) (b :: k). a :~: b

Reasoning helpers

subst1 :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). (a :~: b) -> f a :~: f b Source #

subst2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (c :: k2) (a :: k1) (b :: k1). (a :~: b) -> f a c :~: f b c Source #

Reified evidence of a type class

data Dict (c :: k -> Constraint) (a :: k) where Source #

Evidence for the constraint c a.

Constructors

Dict :: forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a

Type-level naturals

pattern SZ :: () => n ~ 0 => SNat n Source #

pattern SS :: forall np1 n. () => (n + 1) ~ np1 => SNat n -> SNat np1 Source #

fromSNat' :: forall (n :: Nat). SNat n -> Int Source #

sameNat' :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m) Source #

snatPlus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m) Source #

snatMinus :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m) Source #

snatMul :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m) Source #

snatSucc :: forall (n :: Nat). SNat n -> SNat (n + 1) Source #

Type-level lists

type family (l1 :: [a]) ++ (l2 :: [a]) :: [a] where ... Source #

Type-level list append.

Equations

('[] :: [a]) ++ (l2 :: [a]) = l2
(x ': xs :: [a]) ++ (l2 :: [a]) = x ': (xs ++ l2)

type family Replicate (n :: Natural) (a1 :: a) :: [a] where ... Source #

Equations

Replicate 0 (a2 :: a1) = '[] :: [a1]
Replicate n (a2 :: a1) = a2 ': Replicate (n - 1) a2

lemReplicateSucc :: forall {a1} (a2 :: a1) (n :: Natural). (a2 ': Replicate n a2) :~: Replicate (n + 1) a2 Source #

type family MapJust (l :: [a]) = (r :: [Maybe a]) | r -> a l where ... Source #

Equations

MapJust ('[] :: [a]) = '[] :: [Maybe a]
MapJust (x ': xs :: [a]) = 'Just x ': MapJust xs

lemMapJustEmpty :: forall {a} (sh :: [a]). (MapJust sh :~: ('[] :: [Maybe a])) -> sh :~: ('[] :: [a]) Source #

lemMapJustCons :: forall {a} (sh :: [a]) (n :: a) (sh' :: [Maybe a]). (MapJust sh :~: ('Just n ': sh')) -> sh :~: (n ': Tail sh) Source #

type family Head (l :: [k]) :: k where ... Source #

Equations

Head (x ': _1 :: [k]) = x

type family Tail (l :: [a]) :: [a] where ... Source #

Equations

Tail (_1 ': xs :: [a]) = xs

type family Init (l :: [a]) :: [a] where ... Source #

Equations

Init (x ': (y ': xs) :: [a]) = x ': Init (y ': xs)
Init ('[x] :: [a]) = '[] :: [a]

type family Last (l :: [k]) :: k where ... Source #

Equations

Last (x ': (y ': xs) :: [k]) = Last (y ': xs)
Last ('[x] :: [k]) = x

Unsafe

unsafeCoerceRefl :: forall {k} (a :: k) (b :: k). a :~: b Source #

This is just unsafeCoerce Refl, but specialised to only typecheck for actual type equalities. One cannot, e.g. accidentally write this:

foo :: Proxy a -> Proxy b -> a :~: b
foo = unsafeCoerceRefl

which would have been permitted with normal unsafeCoerce, but would have resulted in interesting memory errors at runtime.