Dhall And Higher-Rank Polymorphism

Dhall is a “configuration language”: For programs that generate configuration files. Because sometimes your config/admin files contain repetitions that you wish you could refactor and automate.

But of course that is not why I am showing you this. I have a more theoretical reason LOL.

But first a basic example: I use an automarking script that requires this kind of YAML config file:

marker_files:
  - markA1.hs
  - TestLib.hs
student_files:
  - A1.hs
tests:
  - command: runghc markA1.hs 0
    description: base case
    mark: 0.5
  - command: runghc markA1.hs 1
    description: small case
    mark: 1
  - command: runghc markA1.hs 2
    description: large case
    mark: 1.5

It could be nicely generated by this Dhall script:

-- "let" is good for both type definitions and term definitions.
-- Here is a type definition.
let TestInfo
    : Type
    = { index : Natural, description : Text, mark : Double }

-- This "let" is a value definition.
let infos
    : List TestInfo
    = [ { index = 0, description = "base case", mark = 0.5 }
      , { index = 1, description = "small case", mark = 1.0 }
      , { index = 2, description = "large case", mark = 1.5 }
      ]

let TestItem
    : Type
    = { description : Text, mark : Double, command : Text }

let prog = "markA1.hs"

-- Functions must be lambdas, even when given names.
let makeItem =
      \(s : TestInfo) ->
        { description = s.description
        , mark = s.mark
        , command = "runghc ${prog} ${Natural/show s.index}"
        }

let map = https://prelude.dhall-lang.org/List/map
-- URL means download the code from there.

in  { student_files = [ "A1.hs" ]
    , marker_files = [ prog, "TestLib.hs" ]
    , tests = map TestInfo TestItem makeItem infos
    }

automarking.dhall

Dhall does not perform a lot of type inference; this is because it has a very advanced type system for which type inference is way too hard. Here are the minimum required type annotations:

In lambdas, specify argument types. Example: \(s: Text) -> "hello " ++ s
If the lambda is also polymorphic, specify type variables as extra arguments. My favourite Haskell example three = \x -> [x,x,x] becomes
```
let three = \(a: Type) -> \(x: a) -> [x,x,x]
```
BTW its polymorphic type has an explicit “forall”:
```
forall (a: Type) -> a -> List a
```
Conversely, calling a polymorphic function requires specifying type arguments.

Example: three Text "hello"

Example: map : forall (a: Type) -> forall (b: Type) -> (a -> b) -> List a -> List b
so I had to use it as map TestInfo TestItem makeItem infos

Dhall does not directly allow recursive types or recursive functions. One can actually prove that every Dhall program terminates. (Therefore Dhall cannot cover everything Turing machines can do.)

However, its advanced type system allows coding up many recursive types and functions indirectly. That will be the rest of this lecture!

Higher-Rank Polymorphism

Higher-rank polymorphism means that “forall” can appear anywhere deeply nested in a type, not just at the outermost level.

The usual polymorphic types we have seen so far have outermost forall’s and that’s it, e.g.,

Haskell	`foo :: forall a. a -> (a > a) -> a`
Dhall	`foo : forall (a: Type) -> a -> (a -> a) -> a`

That is called “rank-1 polymorphism”.

“Rank-2 polymorphism” is when an argument type has its own foralls:

Haskell	`bar :: Bool -> (forall b. b -> b) -> Bool`
Dhall	`bar : Bool -> (forall (b: Type) -> b -> b) -> Bool`

If I use foo with a=Bool, then I get (in Dhall-style notation, but Haskell behaves the same way)

foo Bool : Bool -> (Bool -> Bool) -> Bool

so any Bool -> Bool function is fair game for the 2nd argument, e.g., foo Bool True not.

But if I use bar, the 2nd argument has to be polymorphic, e.g., I cannot use not. You can use the parametricity theorem to prove that only the identity function is legal, e.g., bar True (\(b: Type) -> (x: b) -> x).

“Rank-3 polymorphism” is when an argument type is a function type that wants a polymorphic argument! E.g., the “forall c” in this example makes the whole type rank-3:

x_x :: ((forall c. c -> c) -> Bool) -> Bool

You can probably extrapolate to rank-4, rank-5, etc. (If you can’t, no worries, just read on…)

“Higher-rank” means unlimited rank, allowing rank-n for all n. More simply, you can put “forall” at any depth, not just the outermost. (“Rank” just counts depth.)

Impredicativity

Can I instantiate a type variable to a polymorphic type? E.g., is this legal with my three example?

let three = \(a: Type) -> \(x: a) -> [x,x,x]
let IdType : Type = forall (b: Type) -> b -> b
let id : IdType = \(b: Type) -> \(x: b) -> x
in three IdType id : List IdType

If yes, “impredicative polymorphism”; if no, “predicative polymorphism”. Dhall is impredicative. (Haskell defaults to predicative, but you can enable impredicativity per file.)

Inductive Types

Inductive types are recursive types that can be understood like in CSCB36 defining sets by induction. There is also a formal definition:

Terminology: In types of the forms below, the P’s are in “positive” positions, and the N’s are in “negative” positions. Equivalently, function codomains are positive and function domains are negative.

P0
(P0, P1)
Either P0 P1
N1 -> P0
N1 -> (P0, P1)
N1 -> Either P0 P1
N1 -> N2 -> P0
(N1, N2) -> P0

An inductive type is an algebraic data type such that, in field types, recursion occurs in positive positions only. Example and non-example:

data Example = C0 | C1 Example | C2 (Bool -> Example)
data NotInductive = D1 (NotInductive -> ...) | ...

Inductive types can be represented by polymorphic types! How:

Beginner way: Write the function for structural recursion on the inductive type. Then its polymorphic type (omitting the inductive type itself) is the answer.
Pro way: The answer always looks like “forall r. … → r”. Argument types are derived from data constructors.

Each data constructor can be seen as a constant/function with a certain type. Replace every occurence of the inductive type by r. That becomes the corresponding argument type in the answer.

I’ll show you examples.

Lists (of integers)

I will show lists of integers for now. Later I will show lists of a type variable.

In basic Haskell we would have an algebraic data type and its structural recursion:

data DataListZ = Nil | Node Integer DataListZ
    deriving Show

-- Structural recursion. It's foldr but different argument order.
srec :: forall r. DataListZ -> r -> (Integer -> r -> r) -> r
srec xs ifNil ifNode = go xs
  where
    go Nil = ifNil
    go (Node x xt) = ifNode x (go xt)

Inductive.hs

Structural recursion gives the type forall r. r -> (Integer -> r -> r) -> r. The two arguments r and (Integer -> r -> r) can also be derived from the data constructors:

ctor	replace DataListZ by r
`Nil :: DataListZ`	`r`
`Node :: Integer -> DataListZ -> DataListZ`	`Integer -> r -> r`

So here is that representation in Haskell and Dhall:

type InvListZ = forall r. r -> (Integer -> r -> r) -> r

example :: InvListZ
example = \ifNil ifNode -> ifNode 4 (ifNode 1 (ifNode 6 ifNil))

mySum :: InvListZ -> Integer
mySum xs = xs 0 (+)

Inductive.hs

-- ifNil and ifNode derived from data constructors. I call them "ops",
-- package them in a record type.
let Ops
    : Type -> Type
    = \(r : Type) -> { ifNil : r, ifNode : Integer -> r -> r }

let InvListZ
    : Type
    = forall (r : Type) -> Ops r -> r

let example =
      \(r : Type) ->
      \(op : Ops r) ->
        op.ifNode +4 (op.ifNode +1 (op.ifNode +6 op.ifNil))

let Integer/add = https://prelude.dhall-lang.org/Integer/add

let mySum
    : InvListZ -> Integer
    = \(xs : InvListZ) -> xs Integer { ifNil = +0, ifNode = Integer/add }

in  mySum example

InvListZ.dhall

I call it “InvListZ” because it uses inversion of control: As example shows, I don’t give you a data list; instead, you give me the callback operations ifNil and ifNode, and I call them with the right arguments for the right number of times.

Note that the type of mySum is already rank-2 because it expands to (forall r. ...) -> Integer. More complex functions require higher ranks and even impredicativity.

We can prove that InvListZ is in bijection with built-in lists of integers (or Haskell DataListZ). The conversions (in Dhall notation) are:

let toInvListZ
    : List Integer -> InvListZ
    = \(xs : List Integer) ->
      \(r : Type) ->
      \(op : Ops r) ->
        List/fold Integer xs r op.ifNode op.ifNil
        -- Dhall List/fold is foldr but different argument order.

let fromInvListZ
    : InvListZ -> List Integer
    = \(xs : InvListZ) ->
        xs
          (List Integer)
          { ifNil = [] : List Integer
          , ifNode = \(x : Integer) -> \(xs : List Integer) -> [ x ] # xs
          }

InvListZ.dhall

The equations to prove and how are:

fromInvListZ ∘ toInvListZ = id	structural induction on built-in lists
toInvListZ ∘ fromInvListZ = id	parametricity theorem for InvListZ

Lists (of a type variable)

For generic lists that let you specify element types, add a type parameter for the element type, but otherwise similar to the above.

let Ops = \(a : Type) -> \(r : Type) -> { ifNil : r, ifNode : a -> r -> r }

let InvList : Type -> Type
    = \(a : Type) -> forall (r : Type) -> Ops a r -> r

let example : InvList Integer
    = \(r : Type) ->
      \(op : Ops Integer r) ->
        op.ifNode +4 (op.ifNode +1 (op.ifNode +6 op.ifNil))

let length : forall (a : Type) -> InvList a -> Natural
    = \(a : Type) ->
      \(xs : InvList a) ->
        xs Natural { ifNil = 0, ifNode = \(_ : a) -> \(r : Natural) -> 1 + r }

in  length Integer example

InvList.dhall

Similarly in Haskell (see Inductive.hs), just less verbose—fewer type annotations.

Abstract Types

An abstract type is a secret type (users can’t access its internal definition) along with an interface—constants and functions for using it. This is closely related to objects, there are similarities and differences, but I won’t go into them here.

My example is a type s with these functions:

get  : s -> Natural
next : s -> s
init : s

get is a getter. next would be a setter, except that we are in an immutable language, so we settle for a function from old state to new state.

This example happens to represent an infinite sequence of natural numbers! E.g., the 3rd item is get (next (next init)).

To use it, you can write a function that accepts any implementation via arguments:

forall (s : Type) -> { get : s -> Natural, next : s -> s, init : s } -> ReturnType

But then I perform an inversion of control on that! Give me your function of that type, I will call it with my secret implementation:

   (forall (s : Type) -> { get : s -> Natural, next : s -> s, init : s } -> ReturnType)
-> ReturnType

And of course it also needs to work for all ReturnType:

   forall (r : Type)
-> (forall (s : Type) -> { get : s -> Natural, next : s -> s, init : s } -> r)
-> r

That type can be proved (by parametricity) to represent all possible behaviours of the abstract type.

Here is an example of hiding the Fibonacci sequence in that type:

let Methods = \(s : Type) -> { get : s -> Natural, next : s -> s, init : s }

let Stream
    : Type
    = forall (r : Type) -> (forall (s : Type) -> Methods s -> r) -> r

let FibState = { prev : Natural, now : Natural }
let fibGet = \(s : FibState) -> s.now
let fibNext = \(s : FibState) -> { prev = s.now, now = s.prev + s.now }
let fibInit = { prev = 0, now = 1 }
let fibs
    : Stream
    = \(r : Type) ->
      \(user : forall (s : Type) -> Methods s -> r) ->
        user FibState { get = fibGet, next = fibNext, init = fibInit }

let fourth
    : Natural
    = fibs
        Natural
        ( \(s : Type) ->
          \(m : Methods s) ->
            m.get (m.next (m.next (m.next m.init)))
        )

let nthFib
    : Natural -> Natural
    = \(n : Natural) ->
        fibs
          Natural
          ( \(s : Type) ->
            \(m : Methods s) ->
              m.get (Natural/fold n s m.next m.init)
          )

let map = https://prelude.dhall-lang.org/List/map

in  map Natural Natural nthFib [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ]

Stream.dhall

Theory

Polymorphic types are analogous to for-all statements; that’s why researchers feel free to reuse the ∀ symbol.

Abstract types are analogous to exists statements, and researchers feel free to say “existential types” too. An abstract type that supports my example interface can be described as “there exists a type s such that the methods in Method s are available”: ∃s. Method s

Dhall doesn’t have syntax for existential types, but we can get it from higher-rank polymorphism:

Every type T is in bijection with (∀r. (T → r) → r). This is easily proved by parametricity.

So (∃s. Method s) becomes (∀r. ((∃s. Method s) → r) → r).

Analogous to logic, given that r does not use s, ((∃s. Method s) → r) is in bijection with (∀s. Method s → r). You can also see both as describing users.

So the whole thing becomes (∀r. (∀s. Method s → r) → r), which is my stream type.

Haskell has both higher-rank polymorphism and syntax for existential types! You can use either. See Stream.hs.

Epilogue

It is unusual that something practical like a configuration language features something geeky like higher-rank impredicative polymorphism. There are many other configuration languages and none of them are like this.

I haven’t checked with the creator, but I think if you want:

higher-order functions (because map, filter, zip, etc., are super useful)
restrictive enough to guarantee termination
flexible enough to allow inductive types and structural recursion

then your best bet is “second order polymorphic lambda calculus” aka “System F”. (It just means lambdas, static typing, and higher-rank impredicative polymorphism.)

I do not have to add static typing as a wanted, since it is forced on you. You have seen how dynamically typed higher-order functions allow non-termination, so dynamic typing is not an option.

This may be why Dhall started with System F and added practical but safe additions such as numbers, strings, lists, records, and tagged unions.

Or maybe just because the creator, Gabriella Gonzalez, is a well-known Haskeller who just loves all kinds of geeky PLT stuff. 😃