Data.Summer

The extensible sum type and its associated pattern for convenience

data Sum (xs :: [*])

The extensible sum type, allowing inhabitants to be of any of the types in the given type list.

Instances

ApplyFunction ShowTypeable xs => Show (Sum xs)

Showing extensible sums.

Defined in Data.Summer

Methods

showsPrec :: Int -> Sum xs -> ShowS

show :: Sum xs -> String

showList :: [Sum xs] -> ShowS

Generic (Sum xs) => Generic (Sum (x ': xs))

Defined in Data.Summer

Associated Types

type Code (Sum (x ': xs)) :: [[Type]]

Methods

from :: Sum (x ': xs) -> Rep (Sum (x ': xs))

to :: Rep (Sum (x ': xs)) -> Sum (x ': xs)

Generic (Sum ('[] :: [Type]))

Defined in Data.Summer

Associated Types

type Code (Sum '[]) :: [[Type]]

Methods

from :: Sum '[] -> Rep (Sum '[])

to :: Rep (Sum '[]) -> Sum '[]

(Eq (Sum xs), Eq x) => Eq (Sum (x ': xs))

Testing extensible sums for equality.

Defined in Data.Summer

Methods

(==) :: Sum (x ': xs) -> Sum (x ': xs) -> Bool

(/=) :: Sum (x ': xs) -> Sum (x ': xs) -> Bool

Eq (Sum ('[] :: [Type]))

Defined in Data.Summer

Methods

(==) :: Sum '[] -> Sum '[] -> Bool

(/=) :: Sum '[] -> Sum '[] -> Bool

type Code (Sum (x ': xs))

Defined in Data.Summer

type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)

type Code (Sum ('[] :: [Type]))

Defined in Data.Summer

type Code (Sum ('[] :: [Type])) = '[] :: [[Type]]

pattern Inj :: forall x xs. x `HasTagIn` xs => x -> Sum xs

A pattern to match on for convenience. Without this, the user facing interface is rather baroque.

tag :: forall x xs. x `HasTagIn` xs => Word

Computes the tag of the given type in the given type level list.

Construction and Deconstruction

inject :: forall x xs. x `HasTagIn` xs => x -> Sum xs

Injects a type into the extensible sum.

inspect :: forall x xs. x `HasTagIn` xs => Sum xs -> Maybe x

Inspects an extensible sum for a particular type.

consider :: forall x xs. x `HasTagIn` xs => Sum xs -> Either (Sum (Delete x xs)) x

Consider a certain type, discarding it as an option if it is not the correct one.

considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x

Consider the first type in the list of possibilities, a useful specialization for type inference.

variant :: forall a b xs p f. (a `HasTagIn` xs, Applicative f, Choice p) => p a (f b) -> p (Sum xs) (f (Sum (Replace a b xs)))

A prism which operates on a chosen variant of a Sum

class UnorderedMatch xs matcher where

Methods

unorderedMatch :: Sum xs -> matcher

Instances

(Result matcher ~ r, Match (Unmatcher matcher r), Matcher (Unmatcher matcher r) r ~ matcher, HasTagIn y xs, UnorderedMatch (Delete y xs) matcher) => UnorderedMatch xs ((y -> r) -> matcher)

Defined in Data.Summer

Methods

unorderedMatch :: Sum xs -> (y -> r) -> matcher

UnorderedMatch ('[] :: [Type]) r

Defined in Data.Summer

Methods

unorderedMatch :: Sum '[] -> r

class Match xs where

A typeclass for scott encoding extensible sums

Methods

match :: forall r. Sum xs -> Matcher xs r

unmatch :: (forall r. Matcher xs r) -> Sum xs

override :: forall r. r -> Matcher xs r -> Matcher xs r

Instances

Match ('[] :: [Type])

Defined in Data.Summer

Methods

match :: Sum '[] -> Matcher '[] r

unmatch :: (forall r. Matcher '[] r) -> Sum '[]

override :: r -> Matcher '[] r -> Matcher '[] r

(Unmatch xs (x ': xs), Match xs) => Match (x ': xs)

Defined in Data.Summer

Methods

match :: Sum (x ': xs) -> Matcher (x ': xs) r

unmatch :: (forall r. Matcher (x ': xs) r) -> Sum (x ': xs)

override :: r -> Matcher (x ': xs) r -> Matcher (x ': xs) r

class Unmatch xs ys

A utility typeclass which makes the implementation of Match cleaner.

Minimal complete definition

unmatchGo

Instances

Unmatch ('[] :: [Type]) ys

Defined in Data.Summer

Methods

unmatchGo :: Matcher '[] (Sum ys) -> Sum ys

(Unmatch xs ys, HasTagIn x ys) => Unmatch (x ': xs) ys

Defined in Data.Summer

Methods

unmatchGo :: Matcher (x ': xs) (Sum ys) -> Sum ys

Type families

type family TagIn (x :: k) (xs :: [k]) where ...

A type family for computing the tag of a given type in an extensible sum. In practice, this means computing the first index of the given type in the list.

Equations

TagIn x (x ': xs) = 0

TagIn x (y ': xs) = 1 + TagIn x xs

class KnownNat (x `TagIn` xs) => HasTagIn x xs

A class that is used for convenience in order to make certain type signatures read more clearly.

Instances

KnownNat (TagIn x xs) => HasTagIn (x :: k) (xs :: [k])

Defined in Data.Summer

type family Delete (x :: k) (xs :: [k]) :: [k] where ...

A type family for deleting the given type from a list

Equations

Delete x (x ': xs) = xs

Delete x (y ': xs) = y ': Delete x xs

Delete x '[] = '[]

class HaveSameTagsIn xs ys

A class which checks that every type has the same tag in the first list as the second. In other words, checks if the first list is a prefix of the other.

Instances

HaveSameTagsIn ('[] :: [k2]) (ys :: k1)

Defined in Data.Summer

HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs :: [a]) (x ': ys :: [a])

Defined in Data.Summer

type family Matcher xs r :: Type where ...

The scott encoding of an extensible sum

Equations

Matcher '[] r = r

Matcher (x ': xs) r = (x -> r) -> Matcher xs r

Weakening extensible sums

class Weaken xs ys where

Transforming one sum into a sum which contains all of the same types

Methods

weaken :: Sum xs -> Sum ys

Instances

Weaken ('[] :: [Type]) ys

Defined in Data.Summer

Methods

weaken :: Sum '[] -> Sum ys

(Weaken xs ys, HasTagIn x ys) => Weaken (x ': xs) ys

Defined in Data.Summer

Methods

weaken :: Sum (x ': xs) -> Sum ys

noOpWeaken :: forall xs ys. xs `HaveSameTagsIn` ys => Sum xs -> Sum ys

A free version of weakening, where all you're doing is adding more possibilities at exclusively higher tags.

Transforming extensible sums

inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs

Transforms one type in the sum into another.

smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys

Transform one type in one sum into another type in another sum.

Applying Polymorphic Functions

class ForAll c xs => ApplyFunction c xs where

Using functions which only require constraints which are satisfied by all members of the sum.

Methods

apply :: (forall a. c a => a -> y) -> Sum xs -> y

Instances

ApplyFunction c ('[] :: [Type])

Defined in Data.Summer

Methods

apply :: (forall a. c a => a -> y) -> Sum '[] -> y

(c x, ApplyFunction c xs) => ApplyFunction c (x ': xs)

Defined in Data.Summer

Methods

apply :: (forall a. c a => a -> y) -> Sum (x ': xs) -> y

type family ForAll c xs :: Constraint where ...

Equations

ForAll c '[] = ()

ForAll c (x ': xs) = (c x, ForAll c xs)