## Stream: Beginner Questions

### Topic: Polymorphic recursion

#### Jan van Brügge (Apr 26 2021 at 10:48):

Just trying it out naively does not work. Is there are trick or is it not possible to use polymorphic recursion in datatypes?

#### Manuel Eberl (Apr 26 2021 at 10:51):

These are called non-uniform datatypes, and no, the normal datatype package cannot do that.

There's a paper by @Jasmin Blanchette et al. from a few years ago on it though: https://www21.in.tum.de/~traytel/papers/lics17-nonuniform/nonuniform.pdf

#### Manuel Eberl (Apr 26 2021 at 10:52):

(Tagging @Dmitriy Traytel as well)

#### Dmitriy Traytel (Apr 26 2021 at 10:56):

Yes, unfortunately for non-uniform datatypes there is only a partial implementation (which is thus not part of the Isabelle distribution). But the approach described in the linked paper could be nonetheless followed in principle (define a larger uniform (co)datatype first; carve out the more precise non-uniform type via `typedef`; lift definitions and theorems from the too-large uniform type to the non-uniform one).

#### Dmitriy Traytel (Apr 26 2021 at 10:58):

@Jan van Brügge what is the specific non-uniform type you would like to define?

#### Jan van Brügge (Apr 26 2021 at 11:03):

A finger tree:

``````datatype 'a digit = One 'a | Two 'a 'a | Three 'a 'a 'a | Four 'a 'a 'a 'a
datatype 'a node = Node2 'a 'a | Node3 'a 'a 'a
datatype 'a fingertree = Empty | Single 'a | Deep "'a digit" "'a node fingertree" "'a digit"
``````

#### Jan van Brügge (Apr 26 2021 at 11:05):

But I just wanted to quickly check a property of the haskell code, so any heavy encoding is probably not worth it as it strays too far from the original definition

#### Manuel Eberl (Apr 26 2021 at 11:09):

There are finger trees in the AFP: https://www.isa-afp.org/browser_info/current/AFP/Finger-Trees/FingerTree.html

#### Jan van Brügge (Apr 26 2021 at 11:10):

Yes, I saw that, but as said, I tried to prove something about the haskell code, so a completely different definition is not really helpful

#### Dmitriy Traytel (Apr 26 2021 at 14:13):

So following the approach from our paper you would end up with the following definitions

``````datatype 'a digit = One 'a | Two 'a 'a | Three 'a 'a 'a | Four 'a 'a 'a 'a
datatype 'a node = Node2 'a 'a | Node3 'a 'a 'a

datatype (discs_sels) 'a sh = Leaf 'a | Node "'a sh node"
datatype 'a raw = Empty0 | Single0 "'a sh" | Deep0 "('a sh) digit" "'a raw" "('a sh) digit"

inductive ok_sh where
"ok_sh 0 (Leaf x)"
| "pred_node (ok_sh n) s ⟹ ok_sh (Suc n) (Node s)"
monos node.pred_mono

inductive ok where
"ok n Empty0"
| "ok_sh n s ⟹ ok n (Single0 s)"
| "pred_digit (ok_sh n) d1 ⟹ ok (Suc n) t ⟹ pred_digit (ok_sh n) d2 ⟹ ok n (Deep0 d1 t d2)"

primrec flat_sh where
"flat_sh (Leaf x) = Node (map_node Leaf x)"
| "flat_sh (Node t) = Node (map_node flat_sh t)"

primrec flat where
"flat Empty0 = Empty0"
| "flat (Single0 s) = Single0 (flat_sh s)"
| "flat (Deep0 d1 t d2) = Deep0 (map_digit flat_sh d1) (flat t) (map_digit flat_sh d2)"

lemma ok_sh_flat_sh: "ok_sh n s ⟹ ok_sh (Suc n) (flat_sh s)"
by (induct n s rule: ok_sh.induct) (auto intro!: ok_sh.intros simp: node.set_map node.pred_set)

lemma ok_flat: "ok n t ⟹ ok (Suc n) (flat t)"
by (induct n t rule: ok.induct)
(auto intro!: ok.intros simp: digit.set_map digit.pred_set ok_sh_flat_sh)

typedef 'a fingertree = "{t :: 'a raw. ok 0 t}"
by (rule exI[of _ Empty0]) (auto intro: ok.intros)

setup_lifting type_definition_fingertree

lift_definition Empty :: "'a fingertree" is "Empty0"
by (auto intro: ok.intros)

lift_definition Single :: "'a ⇒ 'a fingertree" is "Single0 o Leaf"
by (auto intro: ok.intros ok_sh.intros)

lift_definition Deep :: "'a digit ⇒ 'a node fingertree ⇒ 'a digit ⇒ 'a fingertree" is
"λd1 t d2. Deep0 (map_digit Leaf d1) (flat t) (map_digit Leaf d1)"
by (auto intro!: ok.intros ok_sh.intros simp: digit.set_map digit.pred_set ok_flat)
``````

This possibly falls under what you call "heavy encoding" though. On the other hand the precise definition does not matter; what matters are the properties of Empty, Single, Deep (e.g., injectivity, distinctness) and with a little bit of work (also described in our paper) one can get them---then it does not matter how the type was defined.

Last updated: Aug 10 2022 at 20:22 UTC