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)