A common language for dependently-typed programming?

The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types.

1. Epigram
2. ATS (successor to Dependent ML and Xanadu)
3. Agda (successor to Cayenne)
4. Ωmega
5. NuPrl
6. Twelf
7. Isabelle
8. Coq
9. Delphin
10. Concoqtion
11. Aldor
12. Guru (successor to RSP1)

And now, a list of caveats about the above list:

• Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq.
• This list does not include several languages that are new or new variants (PIE, Matita), not checked at compile-time (Sage), or not actively maintained (most proof assistants, Charity).
• Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Aldor can't understand most type equalities, making its dependent types somewhat weak, though Atypical and Aldor-- aimed to remedy this five years ago. Agda and Epigram have New Exciting Versions 2 coming out, so they suffer from the Osborne Effect.

Is it time yet to do anything about the cornucopia of options? When Haskell began, there were many similar options; the list above is heterogeneous. Is that because it's too early in to tell what the Right choices will be? Is this problem fundamentally harder than the one that inspired the Haskell precursors?

I'm not sure, though deciding how to ensure termination seems particularly tricky. Nonetheless, there are other decisions that aren't as directly related to the central dependent type issues, like syntax, functional purity (though this is related to termination), and editing environment. Maybe these issues will divide the ecosystem into a few niches, each dominated by one player. In the meantime, it's tough to choose.

Lectures on the Curry-Howard Isomorphism saves the day

Morten Heine B. Sørensen and Pawel Urzyczyn's Lectures on the Curry-Howard Isomorphism (mirror 1, mirror 2, errata) provides answers to two questions I asked here before:

I speculated about a complexity problem and its relation to types. On page 104 of LotCHI (92, in print), the authors note that, in the simply-typed lambda calculus, a reduction of the type inhabitation problem to the type checking problem would show that P = PSPACE.

I also wondered if there was a Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that some type is uninhabited. LotCHI section 12.2 gets part of the way there (The authors cover F2, I would need F3, I think.), with the answer that yes, there is such an algebra, but no, it doesn't make things so easy.

Fuzzy Logic and Inuitionistic Logic

I recently got rid of a pop science book on fuzzy logic that I purchased about eight years ago. When I first read it, it seemed to me to be not all that interesting, since it didn't seem like it created any particularly new ways of thinking about things. After all, calling someone "tall" is just shorthand, and it's not exactly revolutionary to call someone "somewhat tall" or "48% tall", since we can do that already when we talk about any continuous domain.

I put the book aside and figured that I either didn't get it, I had picked a bad explanation, or it truly was not something I would be interested in.

It occurs to me now that the idea of indeterminate truth should be very interesting to me, since I'm interested in intuitionistic logic, especially where provability differs from truth. The Stanford Encyclopedia of Philosophy indicates that the fuzzy logic I was thinking of is the "broad sense" or "fuzzy control", and that there's a whole other sense of fuzzy logic that is more closely related to my interests.

Are there any Zero-Knowledge Proofs?

I speculated before about zero-knowledge proofs and existentials. What I had in mind was encoding knowledge hiding via types. I suspect this result would be more interesting than I had imagined. Here is my understanding:

Zero-knowledge proofs are interactive proofs, and are therefore in the class IP. This class is the same as PSPACE, which is not yet known to be distinct from P (though it certainly contains P). So, it's possible that P = IP = PSPACE, and ZK proofs can't hide anything the verifier couldn't calculate herself. In other words, we may one day discover that most of our ZK proof protocols are useless. (This is not the whole story, as there are lots of variations on interactive proving.)

So, if there were a correspondence between these ZK proofs and existential types, it would either settle the P = PSPACE problem or discover a problem in type theory that is equivalent to it.

Each of these seems quite unlikely to me.

There is at least one person, however, who is doing research about the relationship between types and cryptography.

Naming Large Integers is Naming Strong Logics

Scott Aaronson's Who Can Name the Bigger Number? was recently discussed on the programming subreddit. One of the comments noted the Big Number Duel, which was inspired by Aaronson's article. The winning entry in the duel was

The smallest number bigger than any finite number named by an expression in the language of set theory with a googol symbols or less.

I think we can do a little bit better without increasing from 10¹⁰⁰ the number of symbols allowed:

The smallest number bigger than any finite number named by an expression in the language of set theory plus an axiom stating the existence of a proper class of inaccessible cardinals with a googol symbols or less.

Since this theory (ZFC+class of inaccessibles) is stronger than ZFC by itself, I suspect it will define larger integers in the same number of symbols. We could continue along this track by listing larger cardinals and stronger axioms of set theory. This game now becomes essentially Bram Cohen's MineField, in which we are not naming just numbers, but logics.

Besides the Big Number Duel, another test of the "name large integers" game was the C Bignum Bakeoff, which asked contestants to wite a C program that returned a large number. Ralph Loader won by to shoehorning a logic called the Calculus of Constructions into his entry, then simply saying something like "the largest integer definable in the Calculus of Constructions using less than a googol symbols".

The idea of naming finite numbers by extending the strength of not only the working notation but also the working logic is not new; see 0^# and 0^†.

Static Analysis as Grammar Checking

When I explain what I intend to study to friends who don't program, I say something like the text below. I'm still working out the kinks in the analogy, but this is my starting point:

---

When we write, we sometimes make mistakes:

I am hunry when I wake up.

So we invented spelling checkers to catch this simple mistake. We did the same thing for computer languages a long time ago, to catch simple mistakes like spelling errors. And, just as we then invented grammar checkers to catch sentences like:

I am hungrily when I wake up.

that spelling checkers wouldn't catch, we also invented more sophisticated methods to catch more sophisticated mistakes in computer programs.

But grammar rules can sometimes restrict how expressive our sentences are if we wish to speak informally, or to be funny or poetic, or to quote someone famous:

You've got a friend in Pennsylvania.
What price justice?
Hand me a hypodeemic nerdle.

For computer programs, we try to characterize useful patterns (like "rhetorical question" or "implicit subject in imperative" in English) and build sets of rules called type systems. These sets of rules are designed to allow these patterns without allowing incorrect constructions. Type systems require all incorrect constructions to be corrected by the author before a program is run.

At the same time, we can build more permissive tools that look for particular patterns that are likely to be errors, like repeated words or a lowercase letter following a question mark. Anything flagged by the tool as possibly erroneous can be inspected by the author and corrected if necessary.

The goal of all of this work (called static analysis) is to catch bugs in software before it is shipped and bothers users or blows up aerospace equipment.

My goal is to build new static analysis tools to help prevent rocket explosions and Mac commercials.

Leibniz Equality, Decomposition, and Definability

In any interesting logic, there are propositions which are true but not provable. The same goes for intuitionistic logic. By the Curry-Howard correspondence, there are types for which neither the types themselves nor their negations are inhabited in the typed lambda calculus. An example of this is Peirce's law: ∀ p, q . ((p -> q) -> p) -> p. We can use Heyting algebra to show that Peirce's law is not provable in intuitionistic logic. According to John C. Mitchell's Foundations for Programming Languages, problem 4.3.16, we could also show that this is not provable because:

. . . if there us a closed lambda term M:((a -> b) -> a) -> a then there is a closed normal form (the normal form of M) of this type. Show that this implicational formula is not provable by showing there is no closed normal form term of this type.

In Emir Pasalic's PhD thesis, (end of section 4.2.2, page 80 in the PDF, 70 in print), he mentions that it is unknown whether the following type is inhabited:

∀ a, b, c, d . Equal (a,b) (c,d) -> Equal a c

where type equality is defined by Leibniz equality

data Equal a b = Equal (∀ f . f a -> f b)

To avoid dealing with datatypes or pairs, this can be expanded to

∀ a, b, c, d . 
    (∀ f . f (∀ r . (a -> b -> r) -> r) -> f (∀ s . (c -> d -> s) -> s)) 
    ->
    (∀ g . g a -> g c)

In GADTless Programming in Haskell 98 (Section 6, top of page 13) Martin Sulzmann and Meng Wang call this the decomposition law.

Is there some Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that this type is uninhabited?

ε0 in an Ord instance

In my last post, I worked rather hard to approach ε₀, but there is a much simpler way to form a type with an Ord instance that has order type ε₀, according to Trees, Ordinals and Termination (mirror)

import List

data Tree = Node | Tree [Tree]

instance Ord Tree where
    compare Node Node = EQ
    compare Node (Tree _) = LT
    compare (Tree _) Node = GT
    compare (Tree x) (Tree y) = compare (sort x) (sort y)

instance Eq Tree where
    x == y = compare x y == EQ   

Or, according to Ordinal Arithmetic with List Structures (mirror)

data Cons = Nil | Cons Cons Cons

instance Ord Cons where
    compare Nil Nil = EQ
    compare Nil (Cons _ _) = LT
    compare (Cons _ _) Nil = GT
    compare a@(Cons x' y') b@(Cons x y) =
        case compare x' x of
          LT -> compare y' b
          EQ -> compare y' y
          GT -> compare a y

instance Eq Cons where
    x == y = compare x y == EQ

These representations do not help in the general problem of representing all ordinals less than some ordinal κ, but they are much simpler than our previous method.

For trees with larger order types, see What's so special about Kruskal's theorem and the ordinal &Gamma₀ (mirror)

Ord, Countable Ordinals, and an Idea of sigfpe

This post is literate Haskell.

In the comments on my last post about ordinals, sigfpe suggests the following type constructors:

type One = ()
type Two = Either One One
type N = [One]
type Nplus1 = Either N One
type NplusN = Either N N
type NtimesN = (N,N)
type NpowN = [N]
type NpowNplusN = Either NpowN N

The idea is that each of these has an Ord instance defined. I think he's suggesting that the Ord instance for each (ignoring _|_) has an order type that is the same as the ordinal its name corresponds to. I have some quibbles with his implementation, but I really like the idea, and so I'll expand on it below.

I'll start with my disagreements. My first is with the order for NpowN. In NpowN

[[(),()]] > [[()],[(),()]] > [[()],[()],[(),()]] > . . .

or in simpler form

[2] > [1,2] > [1,1,2] > . . .

Since no ordinal has an infinite decreasing sequence, the order type of [N] is not that of an ordinal. For now, we'll just disregard the [] type constructor.

My second quibble is with Times. sigfpe does not make this explicit, but the inference I drew from his examples was that we could define Times as

type Times = (,)

That doesn't quite work, though. Ordinal arithmetic places the least significant part first, but the Ord instance for (,) places the most significant part first.

Now that we have these differences out of the way, let's get to the code.

We'll need these options for type class machinery later.

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-incoherent-instances #-}

Ala sigfpe:

> type One = ()
> type Plus = Either
> type Times = Flip Both
>
> data Both a b = Both a b
> newtype Flip f a b = Flip (f b a)

To define Times, we use a pair datatype with the standard Haskell ordering (see instance Ordinal2 Both below), but apply the newtype Flip, which warrants its own definition, as it will be useful elsewhere.

So far, we can only define finite ordinals. In order to represent larger ordinals, we want to be able to represent an unlimited number of applications of a type constructor to a type.

> data ApplyN f x = More (ApplyN f (f x))
>                 | Stop x

ApplyN does this -- after n applications of More, the type x is wrapped n times in the type constructor f. Essentially, ApplyN f x is f^ω(x).

Our first example of this will be adding one ω times.

> type N = ApplyN (Flip Plus One) One

This should look like (λ x . x + 1)^ω (1).

If ApplyN works as advertized, N should have order type ω under a naive definition of Ord. Unfortunately, it does not. First of all, we can't automatically derive Ord for the type ApplyN, since it uses a type constructor, f, to build a new parameter. We will need

> class Ordinal1 f where
>     comp1 :: Ordinal a => f a -> f a -> Ordering

to describe the contract f must meet to make ApplyN f x ordered. Note that we use the class Ordinal here, which is used only to avoid messing the with Eq requirement on instances for Ord.

> class Ordinal t where
>     comp :: t -> t -> Ordering

The second problem with the naive instance of Ordinal on ApplyN is that each application of More leads to a new type closer to the type we're really talking about. What I mean by this is that, for the case of N, we really want to talk about

Flip Plus One (Flip Plus One (Flip Plus One . . . .

Which we can't directly say in Haskell.

We want to be talking about the type that is the limit. Since we can't do that, to compare two values, we'll compare them at the maximum of their levels. For instance, if we want to compare the values Stop () and More $ More $ Stop $ Flip $ Left $ Flip $ Left (), both of which are of type N, we'll inject the value () into the higher level. To do this, we also need f to be have the property that we can inject into it a value of its type parameter.

> class Container f where
>     inject :: x -> f x

To bring this back to the ordinals, we'll be representing ω^ω as either and ordinal less than ω, or an ordinal less than ω², or an ordinal less than ω³ or …, and to compare two ordinals, we get a representation of each in a common level, then compare them using the comparison for ordinals less than the limiting ordinal of that level.

> instance (Container f, Ordinal1 f) => Ordinal1 (ApplyN f) where
>     comp1 (Stop u) (Stop v) = comp u v
>     comp1 (Stop u) (More v) = comp (Stop (inject u)) v
>     comp1 (More u) (Stop v) = comp u (Stop (inject v))
>     comp1 (More u) (More v) = comp1 u v

We've defined the ordering on ApplyN f so that

comp (Stop x) (More (Stop (inject x))) == EQ

which is what the paragraph above says, but more concise. We've defined an equivalence relation on values of the type ApplyN f t such that x == inject x, so we're off to a good start.

We'll also want inject to be monotone, that is

 x < y ==> inject x < inject y

and for inject to send the order type of the domain not just to some order in the codomain, but to the initial order in the codomain. So, it's easy to write

> injectPlusL :: a -> Plus a b
> injectPlusL x = Left x

or

> instance Container (Flip Plus b) where
>     inject v = Flip (Left v)

Injecting a into a*b is trickier, since we need the second part of the pair to be the minimal possible value in order for the injection range to be the initial part of the order. For this we define

> class Least x where
>     least :: x
> instance Least One where
>     least = ()
> instance Least a => Least (Plus a b) where
>     least = Left least
> instance (Least a, Least b) => Least (Times a b) where
>     least = Flip (Both least least)
> instance Least b => Least (Flip Plus a b) where
>     least = Flip (Left least)
> instance (Least a, Least b) => Least (Flip Times a b) where
>     least = Flip (Flip (Both least least))
> instance Least x => Least (ApplyN f x) where
>     least = Stop least

And we can now write the injection from a to a*b:

> instance (Least a) => Container (Flip Times a) where
>     inject v = Flip (Flip (Both least v))

We also have the trivial

> instance Container (ApplyN f) where
>     inject x = Stop x

Let's write the base instances for Ordinal in as general a way as possible:

> class Ordinal2 f where
>     comp2 :: (Ordinal a, Ordinal b) => f a b -> f a b -> Ordering
> instance Ordinal2 Plus where
>     comp2 (Left _) (Right _) = LT
>     comp2 (Right _) (Left _) = GT
>     comp2 (Left x) (Left y) = comp x y
>     comp2 (Right x) (Right y) = comp x y
> instance Ordinal2 Both where
>     comp2 (Both p q) (Both x y) = 
>         case comp p x of
>           LT -> LT
>           GT -> GT
>           EQ -> comp q y
> instance Ordinal2 f => Ordinal2 (Flip f) where
>     comp2 (Flip x) (Flip y) = comp2 x y
>
> instance Ordinal () where
>     comp _ _ = EQ

And the conversion instances between the n-ary Ordinal instances:

> instance (Ordinal1 f, Ordinal a) => Ordinal (f a) where
>     comp = comp1
> instance (Ordinal2 f, Ordinal a, Ordinal b) => Ordinal (f a b) where
>     comp = comp2
> instance (Ordinal2 f, Ordinal a) => Ordinal1 (f a) where
>     comp1 = comp2

Now let's do some examples. First we check that Ordinal is defined for N:

> n_ok = comp (undefined :: N) (undefined :: N)

ω^ω:

> type NpowN = ApplyN (Flip Times N) One
> npowN_ok = comp (undefined :: NpowN) (undefined :: NpowN)

We can now plug in NpowN into its own definition to get ω^ω * ω = ω^{ω + 1}

> type NpowNplusOne = ApplyN (Flip Times N) NpowN
> nPowNplusOne_ok = comp (undefined :: NpowNplusOne) (undefined :: NpowNplusOne)

or ω^{ω * ω} = ω^ω2:

> type NpowNpow2 = ApplyN (Flip Times NpowN) One
> npowNpow2_ok = comp (undefined :: NpowNpow2) (undefined :: NpowNpow2)

The second method looks more powerful, but continuing it keeps us below ω^ω&omega, so let's use the first method of substituting back in to see if we can get further.

ω^{ω + 2}:

> type NpowNplus2 = ApplyN (Flip Times N) NpowNplusOne
> nPowNplus2_ok = comp (undefined :: NpowNplus2) (undefined :: NpowNplus2)

We can now plug ApplyN back into itself, and extend this to ω^{ω + &omega} = ω^{ω * 2}:

        
> type NpowNtimes2 = ApplyN (ApplyN (Flip Times N)) One
> npowNtimes2_ok = comp (undefined :: NpowNtimes2) (undefined :: NpowNtimes2)

Similarly, ω^{ω * 3}:

        
> type NpowNtimes3 = ApplyN (ApplyN (Flip Times N)) NpowNtimes2
> npowNtimes3_ok = comp (undefined :: NpowNtimes3) (undefined :: NpowNtimes3)

ω^{ω * ω} = ω^ω2, which we apready saw before, can also be written as

        
> type NpowNpow2' = ApplyN (ApplyN (ApplyN (Flip Times N))) One
> npowNpow2'_ok = comp (undefined :: NpowNpow2') (undefined :: NpowNpow2')

ω^{ω2 * ω} = ω^ω3 =

        
> type NpowNpow3 = ApplyN (ApplyN (ApplyN (Flip Times N))) NpowNpow2
> npowNpow3_ok = comp (undefined :: NpowNpow3) (undefined :: NpowNpow3)

ω^ωω:

        
> type NpowNpowN = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) One
> npowNpowN_ok = comp (undefined :: NpowNpowN) (undefined :: NpowNpowN)

ω^{ωω + 1}:

        
> type NpowNpowNplusOne = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) NpowNpowN
> npowNpowNplusOne_ok = comp (undefined :: NpowNpowNplusOne) (undefined :: NpowNpowNplusOne)

We can continue this process up to, but not including, ε₀. We might be able to go further than this, but I'll save that for later.

Thanks to sigfpe for the idea!

Ordinal Notation and Computer Proof

Last ordinal post here

There is an implementation in Coq of the countable ordinals up to Γ₀.

More Proof of Referential Transparency

Previously, I talked about proving referential transparency. The authors of A Persistent Union-Find Data Structure (other version) use Coq to prove imperative functions referentially transparent, and they point out the work of Harold Baker, who designed fast persistent arrays (and here), which they also prove to be referentially transparent. These arrays are even available in Haskell, though wrapped in the IO monad.

The authors of the union-find paper say that their structure is not "purely applicative". I don't actually know what that means, but I suppose it means it's not strictly functional, since it requires in-place modification.

In any case, there are now at least four cases for being able to prove referential transparency so we can use it without wrapping everything in the IO monad:

• Memoization - For memoization in (not just for) Haskell, see this paper by the Simons and Conal Elliott. (mirror 1, mirror 2)
• Diff Arrays
• Splay Trees
• Union-Find

Any other ideas?

Constructability, Uncountability, and ω-Haskell

My last post about the uncountable ordinals ended up on the programming subreddit, where someone who I think is Lennart Augustsson said:

Wow, I didn't realize you could do this. Now I have to wrap my brain around in what sense you can represent uncountable ordinals in Haskell since there are only a countable number of Haskell programs. It must be something like constructive reals...

I think he's exactly right, and I think it has something to do with V=L, models, and how many functions are definable in Haskell. I'm going out of my comfort zone on this, so please correct me if I make any incorrect or nonsensical statements. I'll use as my example the powerset of the natural numbers, which is certainly uncountable, and already definable in Haskell with

data Nat = Z | S Nat
type Powerset t = t -> Bool

From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans. From the viewpoint of Haskell, there are an uncountable number of Haskell functions from the natural numbers to the booleans. But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically. Since every function definable in Haskell has a finite definition and the cardinality of a countable union of finite sets is countable, the function definitions of type Nat -> Bool are countable.

|{f : f <- (N -> 2)_ZFC}| >_ZFC |N|
|{f : f <- (N -> 2)_Haskell}| >_Haskell |N|
|{f : f <- (N -> 2)_Haskell}| =_ZFC Σ_{n <- N} |all n-bit functions from N -> Bool| = |N|

From the viewpoint of Haskell, though, this can't be proven; functions are opaque, so we have no way to order or count them. This might not be true if we use some of the unsafe features of Haskell that would allow us to look at the actual assembly corresponding to a function.

We could, I suppose, imagine a programming language which was not limited to finite-length function definitions. ω-Haskell would not only have types with seemingly uncountable numbers of inhabitants, but each inhabitant would also be definable. Yuk!

Region, Effect and Closure Inference, Part 2

Part 1

Michael Stone was correct in his comments to part 1. Ben Lippmeier elaborated to me in an email:

In those slides,
(%) is the kind of regions.
(!) is the kind of effects.
($) is the kind of closures.

The symbol represents the kind, as well as the name space of the R/E/C variables.
…
I don't have a paper for this stuff at the moment, it's still under development - but the type system is based on some other work that has been around for a while:
The Type and Effect Discipline
Jean-Pierre Talpin, Pierre Jouvelot

Polymorphic Type, Region and Effect Inference
Jean-Pierre Talpin, Pierre Jouvelot

Polymorphic type inference and assignment
(For the closure typing)
Xavier Leroy

The type system is a merge of the ones described in the above two papers, but with some extra stuff added on to make it practical to use in a real compiler.

Ordinals, part 2

Part 1

Peter G. Hancock reminded us of the obvious way to define uncountable ordinals. A rough translation into a single data type, rather than a family:

data Ordinal n = Zero (Nat n)
               | Succ (Ordinal n)
               | forall t . Limit (Less t n) (Ordinal t -> Ordinal n)

The parameter n is the "class" of the ordinal. We need the helper definitions:

data Nat n where
    Z :: Nat Z
    S :: Nat n -> Nat (S n)
data Z
data S n

data Less a b where
    LessZ :: Nat b -> Less Z (S b)
    LessS :: Less a b -> Less (S a) (S b)

embed :: Ordinal n -> Ordinal (S n)
embed (Zero x) = Zero (S x)
embed (Succ x) = Succ (embed x)
embed (Limit e f) = Limit (onemore e) (embed . f)
    where
      onemore :: Less a b -> Less a (S b)
      onemore (LessZ x) = LessZ (S x)
      onemore (LessS p) = LessS (onemore p)

Then we can define the first uncountable ordinal as

omega_1 = Limit (LessS (LessZ Z)) embed

and the sequence of ωs up to ω_ω as

omega_n :: Nat n -> Ordinal n
omega_n Z = Zero Z
omega_n (S n) = Limit (plusone n) embed
    where
      plusone :: Nat n -> Less n (S n)
      plusone Z = LessZ Z
      plusone (S n) = LessS (plusone n)

Hancock has many other interesting ways to represent ordinals, including as surreal numbers (with code), in which we can provide a more precise answer the the question I was originally responding to, What happens when you divide infinite by two? In the case of surreal numbers, you get, simply, ω/2, just as you do with the hyperreals. Hancock also provides a datatype for the ordinals up to Γ₀ without resorting to embedded functions, which means we can do things like computably compare them.

Compiler Proof of Referential Transparency

Programs in languages with mutation can make optimizations that Haskell programs can't, at least not without compiler magic, unsafePerformIO, or wrapping return types in the IO monad. Simple examples that spring to mind are memoization and splay trees. Here, operations that should have no semantic effects (calling a fib function or doing a find on a splay map) do have actual effects. It would be nice if Haskell programmers could write these optimizations and prove them safe with the type system, then use these functions as if they were referentially transparent.

My idea for this a few months ago was to use quotient types, since quotient types equate two actually different things that are functionally the same under some view. A Fibonacci function with a memoization table up to 100 looks the same to a caller as one with no memoized values at all, so they are equal under some quotient.

Other things came up, and I put off this idea for a while, and I have now seen a really cool way for Haskell programmers to deal with local effects. Ben Lippmeier's talk at the SAPLING June 2007 meeting (talk summary) explains region and effect inference for Haskell-like languages without sacrificing referential transparency or having to use the IO monad. This insight wouldn't solve the splay tree issue, because reading a splay tree does modify data that is not local to the reading function, though that modification should be opaque to clients.

I can't wait to see the full paper(s) and the implementation. Until I can, I'll have to settle for the slides from an earlier talk with more motivation.

Existentials and Zero-Knowledge Proofs

When I use "∃ x . P(x)" in typed programming (using intuitionistic logic), I must have in hand an x and a proof of P(x). This is not the case in the classical logic, in which I might have a proof of ∃ x . P(x) without knowing any details of x at all.

This idea that I know such an x exists though I have no knowledge of it reminds me of zero-knowledge proofs. Of course, the zero-knowledge proofs referenced in the Wikipedia article aren't so much proofs as they are assurances with high probability. I looked around for zero-knowledge proofs that were more proof-like, but I didn't find much. I wonder if there is any deeper connection between classical existentials and zero-knowledge proofs?

Conor's Rule?

Edwin Brady writes in "How to write programs in two easy steps", that

I think it's also an area where dependently typed languages like Epigram will shine, because it will one day be possible to write verified interpreters for domain specific languages …

I immediately thought "I can write dependently typed programs right now with GADTs, and I can do so in GHC Haskell, Scala, or the upcoming C#". This is, of course, only mostly true, since none of these does termination checking, and the syntax is awkward.

The same blog post later references Greenspun's Tenth Rule:

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp

and I thought that my programs follow a similar pattern with dependent types: I'm always simulating them informally. Based on Section 6.1: "The Trouble with Faking It" in Conor McBride's Faking It (Simulating Dependent Types in Haskell) (mirror), I wonder if there's any truth to something we might call

Conor's Rule

Any sufficiently complicated Haskell or ML program contains an ad hoc, informally-specified, bug-ridden, half-completed simulation of dependent types.

Definability and Continuity

In How Many Functions are There of Type Bool -> Bool?, I stated "The trick is to remember that if f is continuous, then f _|_ =/= _|_ implies that for all x, f x = f _|_". That is false. It would have been true had I said "… remember that if f is definable in Haskell, then …". The correct statement for continuous functions is: for all x, f x ≥ f _|_. The "≥" here is that used in domain theory to talk about CPOs.

In addition to only considering functions definable in Haskell, I was also only considering flat CPOs, in which each element is comparable only to itself and _|_. An example of a CPO that is not flat:

data Wrap = Wrap Unit
data Unit = Unit

In the CPO Wrap_{_|_}, _|_ < Wrap _|_ < Wrap Unit. Though Wrap_{_|_} has three values, just like Bool_{_|_}, there are only nine functions (continuous or definable in Haskell) of type Wrap_{_|_} -> Bool_{_|_}. Furthermore, there are eleven continuous functions of type Wrap_{_|_} -> Wrap_{_|_}, and all are definable in Haskell. (Thanks to Stefan O'Rear for pointing that out).

Clearly, the codomain isn't treated opaquely as it was in the last post: in order to count functions, we need to know the ordering on the codomain.

I have some more thinking to do about counting, continuity, and definability before I can make any more assertions about the cardinality of function types.

Update:

Stefan O'Rear pointed out an error in which I claimed certain functions were not definable in Haskell, when they actually are. A better example of a function that is continuous but not definable in Haskell is:

parallel_or _ True = True
parallel_or True _ = True
parallel_or False False = False

C++ and GADTs

I just noticed this post about GADTs in C++. It's more about C++'s warts than GADTs, but it's interesting nonetheless.

I also noticed recently, while preparing for my upcoming talk at the theory lunch (mirror, suspected future permalink, presently 404), that because the constructors in the OOP version of GADTs each get their own class, the class name can function as the constructor tag. This leads to what is called the Curiously Recurring Template Pattern in C++. Example:

Haskell	C++
data Nat t where Z :: Nat ZTag S :: Nat n -> Nat (STag n) data ZTag data STag n	template<class T> class nat {}; class zero : nat<zero> {}; template<class N> class succ : nat<succ<N> > { public: succ<N>(nat<N> x) : pred(x) {} nat<N> pred; };

Of course, the tags in the Haskell version could have the same names as the constructors, since the constructor and type namespaces in Haskell are disjoint, but they would still have distinct meanings, unlike in the C++ code.

Types Feed

I have added to the sidebar a feed for the blogs I read about types. I made this feed using Google reader, which also prepared a blog-like interface and an atom feed. Some of my posts will be appearing in the feed, since I both read and am an inhabitant of Planet Haskell.

If I Had Time

Projects I would work on if I had time:

• On Simulating Dependent Types with Guarded Algebraic Datatypes:
  • Automatic lambda lifting for the Haskell syntax.
  • Automatic printing of Scala and C# syntax
  • A lambdabot plugin for lifting types, using GHC-as-a-library.
• Sized lists:
  • Make a cabal-ized, hackage-d sized lists library.
  • Automatically translate the buggy NoFib benchmarks to using sized lists to see if the bugs get caught by the type checker.
• Write Data.Scannable and instance Foldable ((->) a)

Missing Morphisms

I'm a fan of Data.Foldable, and I wonder if it could be extended to function types by way of Bananas in Space: Extending Fold and Unfold to Exponential Types (mirror) or Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism (mirror).

Second, I understand that it may not be possible to give simple types to anamorphisms or hylomorphisms (mirror), but I don't see there can't be a Data.Scannable with paramorphisms.

Finally, I'm not even so sure that we can't give all of the bananas, lenses, envelopes and barbed wire generic (but more strongly typed than SYB) interfaces for even non-regular datatypes with initial algebra semantics (code here).

Update:

I think the first and second questions above are worth bothering the Haskell libaries mailing list about, so I did: Paramorphisms / Data.Scanable? (mirror), Catamorphisms for arrows? (mirror). As before, I expect I'll have to push harder (by actually writing some code) if I want any changes made.

Countable Ordinals in Haskell

In Haskell: What happens when you divide infinity by 2?, Eric Kidd asks:

...
2. Is it possible to represent any other (more interesting and/or more correct) definitions of infinity in Haskell?
3. What’s the best way to think about the infinite ordinals?

The code below is my answer to those questions for countable ordinals only. I'm not sure if it makes sense to talk about representing uncoutable sets on the kind of computers we have now: We can talk about infinite countable sets as computable limits of finite objects, but what would an uncountable set look like? They can't be objects of Nat -> Bool, since every object of this type is represented in some finite number of bits. It seems like we are stuck in a universe where Goedel's V=L is true.

{-# OPTIONS_GHC -fglasgow-exts #-}

{- See:
  http://en.wikipedia.org/wiki/Ordinal_arithmetic
  http://en.wikipedia.org/wiki/Large_countable_ordinals

  To add later:
  http://citeseer.ist.psu.edu/487179.html
-}


module Countable where

data Finite = Z
           | S !Finite

{- A countable ordinal is 0, a successor, or a limit of a countable
  sequence. This definition is weak, as the countable sequence should
  be strictly increasing, but that's hard to express. One way to do so
  would be to interpret (Limit f) as the limit of
  (sum i = 0 to n) (1 + f i). Note: this addition is not commutative.
  This would complicate things, however, so I'll leave it for a later
  extension.
-}
data Ordinal = Zero
            | Succ !Ordinal
            | Limit (Finite -> Ordinal) deriving (Show)

{- I believe that there is no computable Eq or Ord instance for Ordinals.
  Comments?
 
  We make an approximation here by taking the nth value of the limit.
  This calculation is very slow, and, of course, will equate a lot of
  ordinals that are not actually equal.
-}

nth :: Ordinal -> Finite -> Integer
nth Zero _ = 0
nth (Succ x) n = 1+(nth x n)
nth (Limit f) n = nth (f n) n

instance Show (Finite -> Ordinal) where
   show f = show [f Z,
                  f (S Z),
                  f (S (S Z)),
                  f (S (S (S Z)))]

instance Eq Ordinal where
   x == y = (show x) == (show y)

{- The basic ordinal arithmetic. Addition and multiplication are not
  commutative.
-}
addOrdinal :: Ordinal -> Ordinal -> Ordinal
addOrdinal x Zero = x
addOrdinal x (Succ y) = Succ (addOrdinal x y)
addOrdinal x (Limit y) = Limit (\z -> addOrdinal x (y z))

multiplyOrdinal :: Ordinal -> Ordinal -> Ordinal
multiplyOrdinal x Zero = Zero
multiplyOrdinal x (Succ y) = addOrdinal (multiplyOrdinal x y) x
multiplyOrdinal x (Limit y) = Limit (\z -> multiplyOrdinal x (y z))

expOrdinal :: Ordinal -> Ordinal -> Ordinal
expOrdinal x Zero = Succ Zero
expOrdinal x (Succ y) = multiplyOrdinal (expOrdinal x y) x
expOrdinal x (Limit y) = Limit (\z -> expOrdinal x (y z))

-- The first infinite ordinal
finite :: Finite -> Ordinal
finite Z = Zero
finite (S x) = Succ (finite x)

omega = Limit finite

-- Apply a f some number of times, starting at z
apply Zero f z = z
apply (Succ n) f z = f (apply n f z)
apply (Limit g) f z = Limit (\x -> apply (g x) f z)

-- With apply, we have more succinct definitions of arithmetic
addOrdinal' x y = apply y Succ x
multiplyOrdinal' x y = apply y (flip addOrdinal x) Zero
expOrdinal' x y = apply y (flip multiplyOrdinal x) (Succ Zero)

-- Enumerates the fixed points of a function.
fix Zero f = apply omega f Zero
fix (Succ n) f = apply omega f (Succ (fix n f))
fix (Limit g) f = Limit (\x -> fix (g x) f)

-- Some larger ordinals:
epsilon n = fix n (expOrdinal omega)

-- The Veblen heirarchy:
veblen Zero b = expOrdinal omega b
veblen (Succ a) b = fix b (veblen a)
veblen (Limit a) b = Limit (\x -> veblen (a x) b)

-- Feferman-Schutte ordinals
gamma n = fix n (flip veblen Zero)

Quotient Types for Information Hiding

Imagine you're writing a datatype for representing sets. You want to hide the internal representation of sets from clients, but you also want to allow clients to perform any operations as efficiently as if the internal representation were exposed. This is not easy, and it's why Data.Set has 36 functions, when all that are really needed to ensure the meaning of a set ("These elements are distinct") are toList and fromList. Of course, writing member :: Ord a => a -> Set a -> Bool as

member x y = Data.List.elem x (toList y)

is just awful, but the price we pay for efficient member is having to open up the module and break the abstraction if one of the 34 other functions doesn't do exactly what we want. In addition to this pain, there's some danger: functions like mapMonotonic are not really safe, and cannot be made so.

The papers I've been reading about quotient types:

• Bart Jacobs' Quotients in Simple Type Theory
• Aleksey Nogin's Quotient Types: A Modular Approach. (mirror 1, mirror 2)

We could alleviate all of this mess with quotient types. Quotient types allow modules to expose their internals with no danger of breaking abstractions. The quotients are the same as the mathematical quotients in abstract algebra, where they are used frequently. Back on the type theory side, the elimination rule for typing quotients depends not just on types, but on terms, and so requires a type system with dependent types. That's a shame, since dependent types are so tricky to typecheck. It would be great if there were some form of lightweight quotient types that didn't require the full power of dependent types.

The break-the-abstraction vs. lose-efficiency-&-safety issue reminds me of the difference between GADTs and lightweight static capabilities: GADTs are verbose, but they allow the client to safely and efficently operate on datatypes in ways that aren't covered by the library.

How Many Functions are There of Type Bool -> Bool?

This post is incorrect. See the corrections.

Or, rather, how many continuous functions are there of type Bool_{_|_} -> Bool_{_|_}? I count 11, which seems like a strange number. The trick is to remember that if f is continuous, then f _|_ =/= _|_ implies that for all x, f x = f _|_. This gives us only two functions which take _|_ to non-_|_:

one = const True
two = const False

The rest of the continuous functions fill the space Bool -> Bool_{_|_}. Since Bool_{_|_} is of size 3, there are 3² remaining functions, which gives us 9+2 = 11 functions.

We can generalize to say that A_{_|_} -> B_{_|_} has |B| + (|B|+1)^|A| inhabitants.

Bug Reporting

A few months ago, I posted a quandary to haskell-cafe about seemingly ineffable types in GHC: for a certain term, the type inferred by GHCi could not simply be listed in the source code, as this would cause the type checker to complain. I didn't get any bites on my post, and I chalked it up to some complications I didn't understand and no one had time to explain, and I went on to thinking about other things.

Last year, I graded a C++ assignment for a class at the local university (and my alma mater). We required the use of std::set, and a student noticed that he could modify the value of a member of a std::set in place, and the compiler wouldn't complain.

Both of these turn out to be bugs, in GHC and in the C++ standard. The lessons I've learned about programming languages:

1. If something doesn't make sense, investigate. If it turns out you just don't understand something that is the way it is for complicated reasons, you still will have learned something useful.
2. The squeaky wheel gets the grease. I asked the Haskell Cafe about the GHC infelicity, but didn't inquire at the GHC-specific mailing lists, and I didn't keep asking when nobody responded.
3. When you see something funny looking, don't just ask people why it's funny looking. Instead, push things to their logical conclusion, and find a test case that's obviously wrong. This will give people a reason to listen to you.

Foralls, Redexes, and Type Lambdas

In my last post about universally quantified types, I was asking why GHC disallows datatypes like Evil while allowing datatypes like Fine:

data OK (x :: * -> *) where
   OK :: OK x
type Fine = OK Maybe
type Evil = OK (forall (f  :: * -> *) . f)

This seems more confusing when Evil' is just fine:

data OK' (x :: *) where
   OK' :: OK' x
type Fine' = OK' Int
type Evil' = OK' (forall (f  :: *) . f)

Ken Shan answered my question: In the static semantics of the typed lambda calculus, only forms like (Λt:k.r) @ s are redexes. This makes sense to me, but it seems like it's so for simplicity reasons. I expect that this makes the metatheory simpler.

Unfortunately, this makes some things in GHC a pain, since GHC doesn't have type lambdas. SPJ suggests that this is because it makes unification for type inference impossible, but I don't yet understand why. The feature list for EHC indicates that it does support type lambdas, though I haven't tested this.

Update: (29 Jan 2007)

A History of Haskell points to A system of constructor classes (mirror) regarding unification and type lambdas.

Foralls, Kinds with Arrows, and Impredicativity (?)

I can't figure out why the kinding rule for universal quantification in F_ω is:

           C, x : k1 |- y : *
(1)    -----------------------------
       C |- (\forall x : k1 . y) : *

That is, why the type inside the universal quantification must be of kind *.

I would expect the rule to be

            C, x : k1 |- y : k2
(1')    ------------------------------
        C |- (\forall x : k1 . y) : k2

Using (1), I can still get

              C, x : k1 |- y : * -> *
(2)    ------------------------------------------------------
       C |- (\Lambda z : * . \forall x : k1 . y @ z) : * -> *

by eta-expansion, so using (1) instead of (1') doesn't seem to reduce the available power, it just makes the notation more annoying.

I suspect that the reason for (1) instead of (1') has something to do with impredicativity, since (1) is only valid in impredicative systems anyway.

Non-constructive Proofs and Programming

Two excellent examples of programming with non-constructive proofs are given in Simplifying Programs Extracted from Classical Proofs by Yevgeniy Makarov. The examples they give are better than the immediate example I think of: the proof that there are some two irrational numbers x and y such that x^y is rational. This proof is simple to do, but requires some heavy background machinery for rational and irrational numbers. Perhaps I could code this proof by using _|_ for the theorems about rational numbers that I know to be true, but don't wish to prove.

The other two examples of simple non-constructive proofs that I think of are the irrationality of the square root of 2 and the infinitude of the primes. Of course, those are usually stated in non-constructive ways, but they are actually constructive with only a slight bit of tweaking. I haven't read enough of the Makarov paper to see if the simplifications proposed would turn these non-constructive proofs into constructive ones.

Non-constructive Proofs and Productivity

Languages in the Dependent ML family allow users to ensure termination by using a termination metric, a number that is strictly decreasing on recursive calls in the definition of the function.

There is a counterpart to termination for co-recursive structures, where we need to show that a function produces values indefinitely. So, for the Collatz conjecture, we want to show termination for:

collatz n = collatz' n []
collatz' 1 r = 1:r
collatz' n r =
    if n `mod` 2 == 0
    then collatz' (n `div` 2) (n:r)
    else collatz' (3*n + 1) (n:r)

But for the twin prime conjecture we want to show the productivity of:

data Stream a = Stream a (Stream a)
twins = twins' 3
twins' n =
    if (primep n) && (primep (n+2))
    then Stream (n,n+2) (twins' (n+2))
    else twins (n+2)

I don't know if any of the members of the DML family can check productivity. Imagine they could, and imagine we had a non-constructive proof of the twin primes conjecture. Could we use that proof to allow a definition of twins to be marked productive?

Most of the time, we talk about the Curry-Howard correspondence in reference to intuitionist logic and functional programming, but non-constructive proofs of productivity seem like a good way to be able to use more powerful logic in programming, since they don't have to change the implementation of the function they are attached to.

Static Security Assurance From Afar

I work at an e-commerce company. I was thinking today of how typed programming would make our code more reliable, and I began to wonder about using types (or other static assurance methods) to ensure that we don't accidentally reveal information to parties that shouldn't see it. I'm thinking here of the Apollo project (specifically, Translating dependency into parametricity) or Flow Caml. I don't see a way for us to use technology like this when working with other companies.

As an example, we might pass a customer's info to a third party site along with some identifying informaiton about us, to verify the third party that the customer is legit. How can I trust the third party site to not reveal our shared secret to the customer?

I suspect this is a problem for cryptographers, not type theorists. Since much of the information that we deliver to customers is tainted by using secrets to obtain it, static analysis wouldn't help maintain security.

Type (Dis)equality

Type equality is the essential ingredient in guarded algebraic datatypes:

data Z ; data S n ;

data ListGADT a n where
    NilListGADT :: ListGADT a Zero
    ConsListGADT :: a -> ListGADT a n -> ListGADT a (S n)

data TypeEqual a b = . . .
data ListEq a n = NilListEq (TypeEqual n Z)
                | forall m . ConsListEq (TypeEqual n (S m)) a (ListEq a m)

What new power would type disequality bring? It might prevent infinite types.

data WrapList a = forall n . WrapList (ListGADT a n)

cons :: a -> WrapList a -> WrapList a
cons x (WrapList y) = WrapList (Cons x y)

ones = cons 1 ones

Here, the size type inside ones is S (S (S . . . . That's bad. What if we wrote:

data TypeDisEq a b where
    DisEqLess :: DisEq Z (S a)
    DisEqMore :: DisEq (S a) Z
    DisEqInduct :: DisEq a b -> DisEq (S a) (S b)

data ListGADTDisEq a n where
    NilListGADTDisEq :: ListGADTDisEq a Zero
    ConsListGADTDisEq :: a -> ListGADTDisEq a n -> (TypeDisEq n (S n)) -> ListGADTDisEq a (S n)

Now, since the size type inside a ListGADTDisEq can't be one more than itself, it's finite, and we might not be able to form ones. Sadly, that's not true:

data WrapListDisEq a = forall n . WrapListDisEq (ListGADTDisEq a n)

cons' :: a -> WrapListDisEq a -> WrapListDisEq a
cons' x (WrapListDisEq NilListGADTDisEq) = WrapListDisEq (ConsListGADTDisEq x Nil DisEqBase)
cons' x (WrapListDisEq p@(Cons q r s)) = WrapListDisEq (ConsListGADTDisEq x p (DisEqInduct s))

ones' = cons' 1 ones'