Gregory Malecha

2018-11-12 19:45:02 UTC

Hello --

I wanted to ask about the new restrictions on co-inductives. I am trying to

update the interaction trees repository to work with the new restrictions

and I think I've done it correctly, but it seemed a little bit more verbose

than I was anticipating and so I'm wondering if there is a better way to do

it.

The full pull request is here:

https://github.com/DeepSpec/InteractionTrees/pull/26

Essentially the type that was

CoInductive itree (e : Type -> Type) (t : Type) : Type :=

| Ret (_ : t)

| Vis {u} (_ : e t) (_ : u -> itree e t)

| Tau (_ : itree e t).

Has become

Inductive itreeF (itree : Type) (e : Type -> Type) (t : Type) : Type :=

| RetF (_ : t)

| VisF {u} (_ : e t) (_ : u -> itree)

| Tau (_ : itree).

CoInductive itree (e : Type -> Type) (t : Type) : Type :=

{ observe : itreeF (itree e t) e t }.

This makes a lot of sense, the relations work similarly, but the tend to be

a bit more verbose. Essentially, they all get wrapped in something that

looks like:

Inductive EqF (r : relation (itree e t)) : itreeF (itree e t) e t -> itreeF

(itree e t) -> Prop :=

| eq_ret {x} : EqF r (RetF x) (RetF x)

| eq_vis {u} {y : e u} k1 k2}

(_ : forall x : u, r (k1 x) (k2 x))

: EqF r (VisF y k1) (VisF y k2)

| eq_tau {it1 it2}

(_ : r it1 it2)

: EqF r (TauF it1) (TauF it2)

CoInductive Eq (a b : itree e t) : Prop :=

{ observe_eq : EqF a.(observe) b.(observe) }.

Originally, I tried to write this without the observe in the type of Eq

(i.e. eq_ret would have type "forall x, EqF r {| observe := RetF x |} {|

observe := RetF x |}"), but this doesn't seem to work because the

constructors of this form are not helpful unless you can destruct a

co-inductive which is the problem being addressed by the new restriction.

So, back to the original question, is there a better (more convenient) way

to represent this type?

Thanks for any feedback.

I wanted to ask about the new restrictions on co-inductives. I am trying to

update the interaction trees repository to work with the new restrictions

and I think I've done it correctly, but it seemed a little bit more verbose

than I was anticipating and so I'm wondering if there is a better way to do

it.

The full pull request is here:

https://github.com/DeepSpec/InteractionTrees/pull/26

Essentially the type that was

CoInductive itree (e : Type -> Type) (t : Type) : Type :=

| Ret (_ : t)

| Vis {u} (_ : e t) (_ : u -> itree e t)

| Tau (_ : itree e t).

Has become

Inductive itreeF (itree : Type) (e : Type -> Type) (t : Type) : Type :=

| RetF (_ : t)

| VisF {u} (_ : e t) (_ : u -> itree)

| Tau (_ : itree).

CoInductive itree (e : Type -> Type) (t : Type) : Type :=

{ observe : itreeF (itree e t) e t }.

This makes a lot of sense, the relations work similarly, but the tend to be

a bit more verbose. Essentially, they all get wrapped in something that

looks like:

Inductive EqF (r : relation (itree e t)) : itreeF (itree e t) e t -> itreeF

(itree e t) -> Prop :=

| eq_ret {x} : EqF r (RetF x) (RetF x)

| eq_vis {u} {y : e u} k1 k2}

(_ : forall x : u, r (k1 x) (k2 x))

: EqF r (VisF y k1) (VisF y k2)

| eq_tau {it1 it2}

(_ : r it1 it2)

: EqF r (TauF it1) (TauF it2)

CoInductive Eq (a b : itree e t) : Prop :=

{ observe_eq : EqF a.(observe) b.(observe) }.

Originally, I tried to write this without the observe in the type of Eq

(i.e. eq_ret would have type "forall x, EqF r {| observe := RetF x |} {|

observe := RetF x |}"), but this doesn't seem to work because the

constructors of this form are not helpful unless you can destruct a

co-inductive which is the problem being addressed by the new restriction.

So, back to the original question, is there a better (more convenient) way

to represent this type?

Thanks for any feedback.