summer-0.3.7.2: An implementation of extensible products and sums
Copyright(c) Samuel Schlesinger 2020
LicenseMIT
Maintainersgschlesinger@gmail.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Summer

Description

 
Synopsis

The extensible sum type and its associated pattern for convenience

data Sum (xs :: [*]) Source #

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

Instances

Instances details
ApplyFunction ShowTypeable xs => Show (Sum xs) Source #

Showing extensible sums.

Instance details

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)) Source # 
Instance details

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])) Source # 
Instance details

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)) Source #

Testing extensible sums for equality.

Instance details

Defined in Data.Summer

Methods

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

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

Eq (Sum ('[] :: [Type])) Source # 
Instance details

Defined in Data.Summer

Methods

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

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

type Code (Sum (x ': xs)) Source # 
Instance details

Defined in Data.Summer

type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)
type Code (Sum ('[] :: [Type])) Source # 
Instance details

Defined in Data.Summer

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

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

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

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

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 Source #

Injects a type into the extensible sum.

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

Inspects an extensible sum for a particular type.

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

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 Source #

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))) Source #

A prism which operates on a chosen variant of a Sum

class UnorderedMatch xs matcher where Source #

Methods

unorderedMatch :: Sum xs -> matcher Source #

Instances

Instances details
(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) Source # 
Instance details

Defined in Data.Summer

Methods

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

UnorderedMatch ('[] :: [Type]) r Source # 
Instance details

Defined in Data.Summer

Methods

unorderedMatch :: Sum '[] -> r Source #

class Match xs where Source #

A typeclass for scott encoding extensible sums

Methods

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

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

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

Instances

Instances details
Match ('[] :: [Type]) Source # 
Instance details

Defined in Data.Summer

Methods

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

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

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

(Unmatch xs (x ': xs), Match xs) => Match (x ': xs) Source # 
Instance details

Defined in Data.Summer

Methods

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

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

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

class Unmatch xs ys Source #

A utility typeclass which makes the implementation of Match cleaner.

Minimal complete definition

unmatchGo

Instances

Instances details
Unmatch ('[] :: [Type]) ys Source # 
Instance details

Defined in Data.Summer

Methods

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

(Unmatch xs ys, HasTagIn x ys) => Unmatch (x ': xs) ys Source # 
Instance details

Defined in Data.Summer

Methods

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

Type families

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

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 Source #

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

Instances

Instances details
KnownNat (TagIn x xs) => HasTagIn (x :: k) (xs :: [k]) Source # 
Instance details

Defined in Data.Summer

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

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 Source #

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

Instances details
HaveSameTagsIn ('[] :: [k2]) (ys :: k1) Source # 
Instance details

Defined in Data.Summer

HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs :: [a]) (x ': ys :: [a]) Source # 
Instance details

Defined in Data.Summer

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

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 Source #

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

Methods

weaken :: Sum xs -> Sum ys Source #

Instances

Instances details
Weaken ('[] :: [Type]) ys Source # 
Instance details

Defined in Data.Summer

Methods

weaken :: Sum '[] -> Sum ys Source #

(Weaken xs ys, HasTagIn x ys) => Weaken (x ': xs) ys Source # 
Instance details

Defined in Data.Summer

Methods

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

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

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 Source #

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 Source #

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

Applying Polymorphic Functions

class ForAll c xs => ApplyFunction c xs where Source #

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 Source #

Instances

Instances details
ApplyFunction c ('[] :: [Type]) Source # 
Instance details

Defined in Data.Summer

Methods

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

(c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) Source # 
Instance details

Defined in Data.Summer

Methods

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

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

Equations

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