Inside 206-105

Syntax

There are a number of syntactic differences between askhfaspidHKA and Haskell, which we will point out as we proceed in this article. To start with, we note that in askhfaspidHKA, typing is denoted using a single colon (false : Bool); in Haskell, a double colon is used (False :: Bool). Additionally, Haskell has a syntactic restriction, where constructors must be capitalized, while variables must be lower-case.

Similar to my OCaml for Haskellers post, code snippets will have the form:

(* askhfaspidHKA *)
{- Haskell -}

Universes

A universe is a type whose elements are types. askhfaspidHKA sports an infinite hierarchy of universes (e.g. Type (* 0 *) : Type (* 1 *), Type (* 1 *) : Type (* 2 *), and so forth) in order to avoid Girard's paradox. In Haskell only provides two universes: * (pronounced “star”, which can be thought of as Type (* 0 *)), and an implicit universe box (which can be thought of as Type (* 1 *)). Terms of type * are called types (an unfortunate overloading of the term), while terms of type box are called kinds; box cannot be explicitly referred to in programs, so we can avoid having to specify what its type is. We will refer to terms who have a type t :: * as expressions.

Importantly, Haskell’s universes are not cumulative: that is, if Nat is a type (i.e. has the type *), it is not automatically a kind. However, in some cases, partial cumulativity can be achieved using datatype promotion, which constructs a separate kind-level replica of a type, where the data constructors are now type-level constructors. Promotion is also capable of promoting type constructors to kind constructors. Furthermore, the division of universes is reflected in the surface syntax, which is divided into three parts: a language for handling base terms (whose types are not a universe), a language for handling type-level terms, and a language for handling kind-level terms (in the Haskell vernacular, people will often call these types and kinds, even if they're not). In some cases this syntax is overloaded, but in later sections, we will often need to say how a construct is formulated separately for each feature.

One good thing about having only two universes, is there is no need for typical ambiguity or universe constraint solving: you will never get a universe inconsistency from Haskell’s typechecker!

Function types

In askhfaspidHKA, given two types A and B, we can construct the type A -> B denoting functions from A to B (for A and B of any universe). Like askhfaspidHKA, functions with multiple arguments are natively supported using currying. Haskell supports function types for both types (Int -> Int) and kinds (* -> *, often called type constructors) and application by juxtaposition (e.g. f x). (Function types are subsumed by pi types, however, we defer this discussion for later.) However, Haskell has some restrictions on how one may construct functions, and utilizes different syntax when handling types and kinds:

For expressions (with type a -> b where a, b :: *), both direct definitions and lambdas are supported. A direct definition is written in an equational style:

Definition f x := x + x.
f x = x + x

while a lambda is represented using a backslash:

fun x => x + x
\x -> x + x

For type families (with type k1 -> k2 where k1 and k2 are kinds), the lambda syntax is not supported. In fact, no higher-order behavior is permitted at the type-level; while we can directly define appropriately kinded type functions, at the end of the day, these functions must be fully applied or they will be rejected by the type-checker. This is an important restriction to maintain decidability of type inference, as it (along with the lack of cumulativity) means that higher-order unification is not needed. Furthermore, the lack of type-level lambdas means that no eta-rule is necessary (Haskell does not define judgmental equality over expressions).

1. Type synonyms:

   Definition Endo A := A -> A.
   type Endo a = a -> a
   

   Type synonyms are judgmentally equal to their expansions. As mentioned in the introduction, they cannot be partially applied. They were originally intended as a limited syntactic mechanism for making type signatures more readable.

2. Closed type (synonym) families:

   Inductive fcode :=
     | intcode : fcode
     | anycode : fcode.
   Definition interp (c : fcode) : Type := match c with
     | intcode -> bool
     | anycode -> char
   end.
   
   type family F a where
     F Int = Bool
     F a   = Char
   

   While closed type families look like the addition of typecase (and would violate parametricity in that case), this is not the case, as closed type families can only return types. In fact, closed type families correspond to a well-known design pattern in askhfaspidHKA, where one writes inductive data type representing codes of types, and then having an interpretation function which interprets the codes as actual types. As we have stated earlier, Haskell has no direct mechanism for defining functions on types, so this useful pattern had to be supported directly in the type families functionality. Once again, closed type families cannot be partially applied.

   In fact, the closed type family functionality is a bit more expressive than an inductive code. In particular, closed type families support non-linear pattern matches (F a a = Int) and can sometimes reduce a term when no iota reductions are available, because some of the inputs are not known. The reason for this is because closed type families are “evaluated” using unification and constraint-solving, rather than ordinary term reduction as would be the case with codes in askhfaspidHKA. Indeed, nearly all of the “type level computation” one may perform in Haskell, is really just constraint solving. Closed type families are not available in a released version of GHC (yet), but there is a Haskell wiki page describing closed type families in more detail.

3. Open type (synonym) families:

   (* Not directly supported in askhfaspidHKA *)
   
   type family F a
   type instance F Int = Char
   type instance F Char = Int
   

   Unlike closed type families, open type families operate under an open universe, and have no analogue in askhfaspidHKA. Open type families do not support nonlinear matching, and must completely unify to reduce. Additionally, there are number of restrictions on the left-hand side and right-hand side of such families in order maintain decidable type inference. The section of the GHC manual Type instance declarations expands on these limitations.

Both closed and type-level families can be used to implement computation at the type-level of data constructors which were lifted to the type-level via promotion. Unfortunately, any such algorithm must be implemented twice: once at the expression level, and once at the type level. Use of metaprogramming can alleviate some of the boilerplate necessary; see, for example, the singletons library.

Dependent function types (Π-types)

A Π-type is a function type whose codomain type can vary depending on the element of the domain to which the function is applied. Once again, Haskell employs different syntax depending on what universe the domain lives in.

For the class of dependent function types referred to as polymorphic functions (e.g. with type forall a : k, a -> a, where k is a kind), Haskell offers native support, with a twist:

Definition id : forall (A : Type), A -> A := fun A => fun x => x.

id :: a -> a
id = \x -> x

In particular, the standard notation in Haskell is to omit both the type-lambda (at the expression level) and the pi-type (at the type level). The pi-type can be recovered using the explicit universal quantification extension:

id :: forall a. a -> a

However, there is no way to directly explicitly state the type-lambda. When the pi-type is not at the top-level, Haskell requires an explicit type signature with the quantification put in the right place. This requires the rank-2 (or rank-n, depending on the nesting) polymorphism extension:

Definition f : (forall A, A -> A) -> bool := fun g => g bool true.

f :: (forall a. a -> a) -> Bool
f g = g True

Polymorphism is also supported at the kind-level using the kind polymorphism extension. However, there is no explicit forall for kind variables; you must simply mention a kind variable in a kind signature.

Proper dependent types cannot be supported directly, but some modicum of support can be achieved by first promoting data types from the expression level to the type-level. This pattern of programming in Haskell is not standard, though there are recent academic papers describing how to employ it. One particularly good one is Hasochism: The Pleasure and Pain of Dependently Typed Haskell Program, by Sam Lindley and Conor McBride.

Product types

askhfaspidHKA supports cartesian product over types, as well as a nullary product type called unit. These constructs are also implemented in the Haskell standard library:

(true, false) : bool * bool
(True, False) :: (Bool, Bool)

tt : unit
() :: ()

Pairs can be destructed using pattern-matching:

match p where
  | (x, y) => ...
end

case p of
  (x, y) -> ...

Dependent pattern match is not supported by Haskell. In some type theories, the meaning of products is defined by way of eliminators; in Haskell, this eliminator is called uncurry.

Dependent pair types (Σ-types)

Dependent pair types are the generalization of product types to be dependent. As before, Σ-types cannot be directly expressed, except in the case where the first component is a type. In this case, there is an encoding trick utilizing data types which can be used to express so-called existential types:

Definition p := exist bool not : { A : Type & A -> bool}

data Ex = forall a. Ex (a -> Bool)
p = Ex not

As was the case with polymorphism, the type argument to the dependent pair is implicit. It can be specified explicitly by way of an appropriately placed type annotation.

Recursion

In askhfaspidHKA, all recursive functions must have a structurally decreasing argument, in order to ensure that all functions terminate. In Haskell, this restriction is lifted for the expression level; as a result, expression level functions may not terminate. At the type-level, by default, Haskell enforces that type level computation is decidable. However, this restriction can be lifted using the UndecidableInstances flag. It is generally believed that undecidable instances cannot be used to cause a violation of type safety, as nonterminating instances would simply cause the compiler to loop infinitely, and due to the fact that in Haskell, types cannot (directly) cause a change in runtime behavior.

Inductive types

Both askhfaspidHKA and Haskell have support for defining inductive data types. Haskell is more flexible than askhfaspidHKA in some ways and less flexible in others.

Basic inductive types like boolean can be defined with ease in both languages (in all cases, we will use the GADT syntax for Haskell data-types, as it is closer in form to askhfaspidHKA’s syntax and strictly more powerful):

Inductive bool : Type :=
  | true : bool
  | false : bool.

data Bool :: * where
  True :: Bool
  False :: Bool

Haskell’s inductive data types support parameters, but these parameters may only be types, and not values. (Though, recall that data types can be promoted to the type level). Thus, the standard type family of vectors may be defined, assuming an appropriate type-level nat (as usual, explicit forall has been omitted):

Inductive vec (A : Type) : nat -> Type :=
  | vnil  : vec A 0
  | vcons : forall n, A -> vec A n -> vec A (S n)

data Vec :: Nat -> * -> * where
  VNil  :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

As type-level lambda is not supported but partial application of data types is (in contrast to type families), the order of arguments in the type must be chosen with care. (One could define a type-level flip, but they would not be able to partially apply it.)

Haskell inductive definitions do not have the strict positivity requirement, since we are not requiring termination; thus, peculiar data types that would not be allowed in askhfaspidHKA can be written:

data Free f a where
   Free :: f (Free f a) -> Free f a
   Pure :: a -> Free f a

data Mu f where
   Roll :: f (Mu f) -> Mu f

Inference

askhfaspidHKA has support for requesting that a term be inferred by the unification engine, either by placing an underscore in a context, or by designing an argument as implicit (how one might implement in askhfaspidHKA the omission of type arguments of polymorphic functions as seen in Haskell). Generally, one cannot expect all inference problems in a dependently typed language to be solvable, and the inner-workings of askhfaspidHKA’s unification engines (plural!) are considered a black art (no worry, as the trusted kernel will verify that the inferred arguments are well-typed).

Haskell as specified in Haskell'98 enjoys principal types and full type inference under Hindley-Milner. However, to recover many of the advanced features enjoyed by askhfaspidHKA, Haskell has added numerous extensions which cannot be easily accomodated by Hindley-Milner, including type-class constraints, multiparameter type classes, GADTs and type families. The current state-of-the-art is an algorithm called OutsideIn(X). With these features, there are no completeness guarantee. However, if the inference algorithm accepts a definition, then that definition has a principal type and that type is the type the algorithm found.

Conclusion

This article started as a joke over in OPLSS'13, where I found myself explaining some of the hairier aspects of Haskell’s type system to Jason Gross, who had internalized askhfaspidHKA before he had learned much Haskell. Its construction was iced for a while, but later I realized that I could pattern the post off of the first chapter of the homotopy type theory book. While I am not sure how useful this document will be for learning Haskell, I think it suggests a very interesting way of mentally organizing many of Haskell’s more intricate type-system features. Are proper dependent types simpler? Hell yes. But it’s also worth thinking about where Haskell goes further than most existing dependently typed languages...