Polymorphic recursion · Beginner Questions

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.

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

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):

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):

Manuel Eberl (Apr 26 2021 at 11:10):

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.

Stream: Beginner Questions

Topic: Polymorphic recursion

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