Theory.Lists

Basic functions on lists

head :: Fact (IsCons xs) => ([a] ~~ xs) -> a ~~ Head xs

Extract the first element from a non-empty list.

tail :: Fact (IsCons xs) => ([a] ~~ xs) -> [a] ~~ Tail xs

Extract all but the first element from a non-empty list.

cons :: (a ~~ x) -> ([a] ~~ xs) -> [a] ~~ Cons' x xs

Construct a list from an element and another list.

nil :: [a] ~~ Nil'

The empty list, named Nil'.

Names for parts of a list

data Head xs

Names for the parts of a list.

data Tail xs

Names for basic list operations

data Cons' x xs

A name for referring to the result of a cons operation.

data Nil'

A name for referring to the empty list.

Reasoning about lists

Predicates about list shapes

data IsList xs

Predicates about the possible shapes of lists.

data IsCons xs

data IsNil xs

Axioms about list shapes

consIsList :: Proof (IsCons xs) -> Proof (IsList xs)

nilIsList :: Proof (IsNil xs) -> Proof (IsList xs)

listIsList :: ([a] ~~ xs) -> Proof (IsList xs)

listShapes :: Proof (IsList xs) -> Proof ((IsNil xs && Not (IsCons xs)) || (IsCons xs && Not (IsNil xs)))

Axiom: a list xs satisfies exactly one of IsCons xs or IsNil xs.

consIsCons :: Proof (IsCons (Cons' x xs))

Axiom: The result of cons x y satisfies IsCons.

headOfCons :: Proof (Head (Cons' x xs) == x)

Axiom: The head of cons x y is x.

tailOfCons :: Proof (Tail (Cons' x xs) == xs)

Axiom: The tail of cons x y is y.

Induction principle

listInduction :: Proof (IsList xs) -> Proof (p Nil') -> Proof (ForAll ys ((IsList ys && p (Tail ys)) --> p ys)) -> Proof (p xs)

Induction principle: If a predicate P is true for the empty list, and P is true for a list whenever it is true for the tail of the list, then P is true.

Pattern-matching on lists

Decompositions that use explicit evidence-passing

classify :: ([a] ~~ xs) -> ListCase a xs

Classify a named list by shape, producing evidence that the list matches the corresponding case.

data ListCase a xs

Possible shapes of a list, along with evidence that the list has the given shape.

Constructors

IsCons_ (Proof (IsCons xs)) (a ~~ Head xs) ([a] ~~ Tail xs)

IsNil_ (Proof (IsNil xs))

Pattern synonyms

pattern IsCons :: Proof (IsCons xs) -> (a ~~ Head xs) -> ([a] ~~ Tail xs) -> [a] ~~ xs

pattern IsNil :: Proof (IsNil xs) -> [a] ~~ xs

Decompositions that use implicit evidence-passing

classify' :: forall a xs. ([a] ~~ xs) -> ListCase' a xs

Classify a named list by shape, producing implicit evidence that the list matches the corresponding case.

data ListCase' a xs where

A variation on ListCase that passes the shape facts implicitly. Pattern-matching on a constructor of ListCase' will bring a shape proof into the implicit context.

Constructors

Cons_ :: Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ListCase' a xs

Nil_ :: Fact (IsNil xs) => ListCase' a xs

Pattern synonyms

pattern Cons :: () => Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> [a] ~~ xs

pattern Nil :: () => Fact (IsNil xs) => [a] ~~ xs