General recursion for non-coinductive types

[takanuva]

Hello,

I'm working on a translation from the calculus of constructions to static single assignment form (then I'll move further to typed assembly). As of now, all SSA programs halt (as expected, since all CoC programs halt).

Though I've got some insight from this paper, I'm still not sure how I'll properly model general recursion (then I assume I'll need one single intrinsic function iter which loops over a coinductive type forever, or until it halts). I'm still confused with that, though.

I'd like to ask how you picture implementing that. Let's assume a Haskell to Morte compiler. A simple recursive function:

fib :: Int -> Int
fib n = if n < 2 then
          return 1
        else
          fib (n - 1) + fib (n - 2)

Or even a mutually recursive function (also assume it's taken from source code, and we can't know if it halts):

is_even :: Int -> Bool
is_even n = if n == 0 then
              True
            else
              is_odd (n - 1)

is_odd :: Int -> Bool
is_odd n = if n == 0 then
             False
           else
             is_even (n - 1)

So, neither Int nor Bool are coinductive types... Do you have any insight on that? (The article claims partiality with coinductive types is a monad. I'm not sure I understood how; I don't know category theory. 😢)

[Gabriella439]

The data type itself enforces the recursion scheme that you use. For example, if you encode Int as a church-encoded peano numeral, like this:

$ cat ./Nat
∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat

... then you have to implement isEven and isOdd on Nat using simple recursion:

$ cat ./isEven
λ(n : ./Nat) → n ./Bool ./not ./True

... assuming that you have the following definitions:

$ cat ./Bool
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
$ cat ./True
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
$ cat ./False
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
$ cat ./not
λ(b : ./Bool) → λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → b Bool False True

You should check out these posts of mine:

• http://www.haskellforall.com/2015/05/the-internet-of-code.html
• http://www.haskellforall.com/2016/04/data-is-code.html

... and this paper, which they are based on:

• http://www.sciencedirect.com/science/article/pii/0304397585901355

[takanuva]

I do understand that I could implement isEven or isOdd this way; I'm asking from the point of view of a Haskell to Morte compiler. The compiler wouldn't be able to infer such things in the general case, specially because the function being compiled could never halt.

Have you thought how would you implement such general recursion on a compiler that generates Morte code? In Morte tutorial, you mention that this may be encoded as state machines, but then the backend would need to be able to detect such state machines to generate assembly code. I believe your Annah language can only deal with code that always halts, right?

[Gabriella439]

I think you are mixing too many concepts at once. Let's simplify the example so that it's just about mutual recursion and nothing else. I'll use this modified version of your original example:

data Nat = Succ Nat | Zero

isEven :: Nat -> Bool
isEven Zero = True
isEven (Succ n) = isOdd n

isOdd :: Nat -> Bool
isOdd Zero = False
isOdd (Succ n) = isEven n

So the question is: can we translate mutual recursive functions like isEven and isOdd to System F?

I'm actually not sure. The paper I linked provides some guidance, particularly in sections 2 and 5, but there is one step that I'm not sure about. I'll explain as much as I do know.

I think the process is roughly the following steps:

• Step 1: Transform your mutually recursive functions so that they are operating on separate (possibly mutually recursive) data types, like this:

data Nat0 = Succ0 Nat1 | Zero0
data Nat1 = Succ1 Nat0 | Zero1

data Bool0 = True0 | False0
data Bool1 = True1 | False1

isEven :: Nat0 -> Bool1
isEven Zero0 = True
isEven (Succ0 n) = isOdd n

isOdd :: Nat1 -> Bool
isOdd Zero1 = False
isOdd (Succ1 n) = isEven n

• Step 2: transform each function into a standard form where you a family of functions (denoted h in the paper) to mutually recursive function calls

data Nat0 = Succ0 Nat1 | Zero0
data Nat1 = Succ1 Nat0 | Zero1

h0 = True
h1 = \x -> x
h2 = False
h3 = \x -> x

isEven :: Nat -> Bool
isEven Zero0 = h0
isEven (Succ0 n) = h1 (isOdd n)

isOdd :: Nat -> Bool
isOdd Zero1 = h2
isOdd (Succ1 n) = h3 (isEven n)

• Step 3: Generate the non-recursive form by following the instructions in sections 2.1 and 5.5 of the paper

This generates something like this:

./Bool =
  ∀(Bool : Type)
→ ∀(True : Bool)
→ ∀(False : Bool)
→ Bool

./True =
  λ(Bool : Type)
→ λ(True : Bool)
→ λ(False : Bool)
→ True

./False =
  λ(Bool : Type)
→ λ(True : Bool)
→ λ(False : Bool)
→ False

./Nat0 =
  ∀(Nat0 : Type)
→ ∀(Nat1 : Type)
→ ∀(h0 : Nat0)
→ ∀(h1 : Nat1 → Nat0)
→ ∀(h2 : Nat1)
→ ∀(h3 : Nat0 → Nat1)
→ Nat0

./Nat1 =
  ∀(Nat0 : Type)
→ ∀(Nat1 : Type)
→ ∀(h0 : Nat0)
→ ∀(h1 : Nat1 → Nat0)
→ ∀(h2 : Nat1)
→ ∀(h3 : Nat0 → Nat1)
→ Nat1

./Q1 = ./Bool

./Q2 = ./Bool

./h0 = ./True

./h1 = λ(x : /Bool) → x

./h2 = ./False

./h3 = λ(x : ./Bool) → x

-- isEven : ./Nat0 → Bool
./isEven = λ(v : ./Nat0 ) → v ./Q1 ./Q2 ./h0 ./h1 ./h2 ./h3

-- isOdd : ./Nat1 → Bool
./isOdd = λ(v : ./Nat1 ) → v ./Q1 ./Q2 ./h0 ./h1 ./h2 ./h3

This generates (almost) the same lambda expression for both functions. I believe this is normal and expected, because we have one last step:

• Step 4 - Generate a function from our original type (i.e. Nat) to the two mutually recursive types (i.e. Nat0 and Nat1)

This is basically where all the real work is done, but it's not clear to me how to automate it. I know how to do it for this specific example, but I'm not sure how to do it in general. To keep the code short I'll use dhall syntax which provides nicer records support:

./Nat =
  ∀(Nat : Type)
→ ∀(Succ : Nat → Nat)
→ ∀(Zero : Nat)
→ Nat

-- ./toNat0 : ./Nat → ./Nat0
./toNat0 =
    λ(n : ∀(Nat : Type) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat)
→   λ(Nat0 : Type)
→   λ(Nat1 : Type)
→   λ(Succ0 : Nat1 → Nat0)
→   λ(Zero0 : Nat0)
→   λ(Succ1 : Nat0 → Nat1)
→   λ(Zero1 : Nat1)
→   (   n
        { _1 : Nat0 , _2 : Nat1  }
        (   λ(x : { _1 : Nat0 , _2 : Nat1 })
        →   { _1 = Succ0 (x._2) , _2 = Succ1 (x._1) }
        )
        { _1 = Zero0, _2 = Zero1 }
    )._1

-- ./toNat1 : ./Nat → ./Nat0
./toNat1 =
    λ(n : ∀(Nat : Type) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat)
→   λ(Nat0 : Type)
→   λ(Nat1 : Type)
→   λ(Succ0 : Nat1 → Nat0)
→   λ(Zero0 : Nat0)
→   λ(Succ1 : Nat0 → Nat1)
→   λ(Zero1 : Nat1)
→   (   n
        { _1 : Nat0 , _2 : Nat1  }
        (   λ(x : { _1 : Nat0 , _2 : Nat1 })
        →   { _1 = Succ0 (x._2) , _2 = Succ1 (x._1) }
        )
        { _1 = Zero0, _2 = Zero1 }
    )._2

I'm not sure if there is a better or mechanical way to do this part, though

I might also be misunderstanding the paper and there might be a better and more direct way to translate mutually recursive functions

[ChristopherKing42]

Is it possible to form a fixed point combinator in such a way that it only works if the function is structurally recursive? From there, mutual recursion should be easy.

[Gabriella439]

You can define a least fixed point type in morte like this:

∀(f : * → *) → ∀(x : *) → (f x → x) → x

... or using Haskell notation:

newtype LFix f = MakeLFix (forall x . (f x -> x) -> x)

... and you can encode a structurally recursive type in a non-recursive way using that encoding