Jason (jcreed) wrote,

Man I feel like I forgot a basic thing about mutually recursive types and church encodings that I am supposed to know.

Consider the type "option A".
  data option (A : Set) : Set where
        NONE : option A
        SOME : A → option A

It supports a recursion operator

option-rec : (C : Set) → C → (A → C) → option A → C

right? Given any result type C, a value of that type to use for NONE, and a function that takes any A and converts it to that result type to use for SOME, and a value of the option type, I can give you a C.

Furthermore, consider defining the natural numbers like so:
data Nat : Set where
     inj : option Nat → Nat

Zero is represented by inj NONE, and successor by inj o SOME.

This datatype immediately supports a recursion operator
nat-rec : (C : Set) → (option Nat → C) → Nat → C

but I also really want to know that it supports the "real" recursion operator for natural numbers:
nat-rec2 : (C : Set) → C → (C → C) → Nat → C

Is there a way I can implement nat-rec2 from option-rec and nat-rec? Is there a stronger principle I can prove of option-rec that will make it possible?
Tags: math, types
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded