Types, named (was: "Name that type!"), plus two more questions

Here are the answers to the previous quiz.

The first datatype holds any factorial number of values. Here it is again, with one small change and a few de-obfuscations:

> data FacHelp (f :: * -> *) (y :: *) = 
>      Stop y
>    | More (FacHelp (OneMore f) (f y))
> newtype OneMore (f :: * -> *) (y :: *) = 
>      OneMore (y, f y)
> newtype Identity y = Identity y
> type Factorial y = FacHelp Identity y

The second is lists of length more than two containing lists of length more than two. This means that no inhabitant contains a prime number of elements. As far as I know, it is unknown whether there is a datatype with every inhabitant containing a prime number of elements. (GADTs can do it, of course, but I'm ignoring those for now, since they can do anything. (mirror, mirror 2, mirror 3, mirror 4)

Here's that datatype again, renamed:

> data LongList x = Two x x
>                 | AndAnother x (LongList x)
> data Composite x = Composite (LongList (LongList x))

Update:
Chung-chieh Shan pointed out to me that I got that datatype wrong. (The other text above is correct, I think.) Anyway, here's his counterexample:

> test :: Composite Char
> test = Composite (Two (Two 'a' 'b')
>                       (AndAnother 'c' (Two 'd' 'e')))

This is a correct (I think!) implementation of a container that can't be of a prime size:

> data Product f g a = Times (f (g a))
>                    | LeftIncr (Product (OneMore f) g a)
>                    | RightIncr (Product f (OneMore g) a)
> newtype Pair a = Pair (a,a)
> type Comp = Product Pair Pair

End update

The third datatype uses the type H, which encodes containers with a square number of elements. H is based on the idea that the sequence of partial sums of the sequence of odd natural numbers is the same as the sequence of squares. That is, {0, 1, 1+3, 1+3+5, …} = {0², 1², 2², 3², …}

We can now use Lagrange's four-square theorem to see that question 3(b) is, strangely, a container that can hold any number of elements. An extension of this by Legendre showed [cite] that every number not of the form 4^k(8m + 7) is representable by the sum of three squares, and this answers question 3(a).

Here are both parts again, renamed and cleaned up a bit:

> data SqHelp x y = End
>                 | Extra x (SqHelp (y,y,x) y)
> type Square a = SqHelp a a
> data Legendre x = Legendre (Square x) (Square x) (Square x)
> data Lagrange x = Lagrange (Square x) (Legendre x)

Here are two more questions:
4. Can we write something analogous to 3(a) in a more direct way?
5.

> data M a b = N b
>            | O (M (a,b) a)
> newtype P a = P (M a a)

Name that type! (nested types edition)

Jump to the bottom for the quiz

If we want to write a type for binary trees in Haskell, it is easy to do so:

> data BinaryTree a = Leaf
>                   | InternalNode (BinaryTree a) a (BinaryTree a)

The structure of the type guarantees certain things about its inhabitants. For instance, every node has exactly two children. If we want to guarantee stronger invariants, we can change the shape of the type. We can write a a type for complete binary tree (that is, binary trees in which every leaf is at the same depth), as

> data CompleteBinaryTree a = Leaves
>                           | NonLeaves a (CompleteBinaryTree (a,a))

The argument in the recursive part of this datatype is not the same as it is in the declaration. Datatypes with this property are called nested or non-regular or heterogeneous or non-uniform. We can express all sorts of invariants with these datatypes. Here's another example:

> data AList a b = Nil
>                | Cons a (AList b a)

If we want to manipulate lists that alternate between two types a and b, we could use the type [Either a b], but this doesn't ensure that we don't have two as or two bs in a row. We could, instead, use the type [(a,b)], but this would only allow us to create lists of even length. By switching the position of the parameters in the recursion in AList, we can represent alternating lists of any length.

Here are some other examples of data structure invariants we can ensure with nested types:

• Cyclic data structures (mirror)
• Many different types of lists with fast cons, snoc, concatenation, and indexing, including
  • Finger trees (mirror, mirror 2)
  • Binary random-access lists, catenable lists, and catenable deques (earlier version, earlier version mirror, earlier version mirror 2, notes and answers to exercises)
  • Rightist right-perfect trees (mirror)
    • earlier version, earlier version mirror, earlier version mirror 2
    • even earlier version, even earlier version mirror, even earlier version mirror 2
• Red-black trees (a paper, code for that paper), AVL trees (mirror, mirror 2)
• Square matrices, triangular matrices (in various works by Ralph Matthes), Toeplitz matrices, rectangular matrices (see "Manufacturing Datatypes", above)
• Efficient-merge heaps (see Okasaki's thesis & book, above), Braun trees, left-complete trees (see "Manufacturing Datatypes", above)
• Binomial queues (mirror, mirror 2)
• Tries (mirror, mirror 2, code, code mirror, old version, old version mirror) (See also Okasaki's thesis & book)
• Well-formed terms in the locally-nameless lambda calculus (mirror)

Finally, here are 3.5 examples of nested types I haven't seen elsewhere. See if you can figure out what they do.

> data A x y = B (x y)
>            | C (A (D x) (x y))
> newtype D x y = D (y,x y)
> newtype K x = K x
> type QuestionOne = A K
>
> data E x = F x x
>          | G x (E x)
> data QuestionTwo x = Q2 (E (E x))
>
> data H x y = I
>            | J y x x (H (y,x) y)
> type L = H ()
> data QuestionThreePartA x = Q3a (L x) (L x) (L x)
> data QuestionThreePartB x = Q3b (L x) (QuestionThreePartA x)

Leibniz and Liskov

Leibniz equality of two types a and b is the proposition that in any context, one can be substituted for the other:

f a -> f b

A value of this type brings to the value level the proof that two types are equal. The only value of this type is the identity function.

The Liskov substitution principle is very similar to Leibniz equality, but only in the contravariant position: If a function takes an argument of type b and a is a subtype of b, then the function must accept an argument of type a. If f is a type constructor that uses its argument only negatively, then a is a subtype of b if there is a value of type

f b -> f a

For example, λx . x -> b uses x negatively, and any b -> b is also trivially an a -> b when a is a subtype of b. The only value of type f b -> f a is the cast function.

Let's write the kind for type constructors that use their argument negatively as * -(-)-> * rather than just * -> *, and the kind for type constructors that use their argument positively as * -(+)-> *. Then, the following terms should validate our understanding that supertyping is dual to subtyping:

dual : ∀ a:* . ∀ b:* . ∀ g: * -(+)-> * . (∀ f: * -(-)-> * .  f b -> f a) -> g a -> g b
dual |a |b |g less bot = less [λx:* . g x -> g b] (λy:g b . y:g b) bot

dual' : ∀ a:* . ∀ b:* . ∀ f: * -(-)-> * . (∀ g: * -(+)-> * . g a -> g b) -> f b -> f a
dual' |a |b |f more top = more [λx:* . f x -> f a] (λy:f a . y:f a) top

So subtyping, like type equality, can be brought to the value domain. I now have two questions:

1. Is there an analogue of F_C (mirror) for F_<: (mirror 1, mirror 2, mirror 3)?
2. Is there a problem similar to decomposition for Liskov substitutability?