How do I encode my datatype?

[zmactep]

trafficstars

Hi, @Gabriel439 !

I have a weird datatype like this one:

data WList a = WNil | WCons a (WList Bool)

How can I encode it in CoC/Morte?

[Gabriella439]

For that specific datatype you can cheat by encoding it as two separate data types. First you encode WList Bool and then you encode WList a in terms of WList Bool, like this:

$ cat WListBool
∀(WList : *) → ∀(WNil : WList) → ∀(WCons : Bool → WList → WList) → WList
$ cat WList
λ(a : *) → ∀(WList : *) → ∀(WNil: WList) → ∀(WCons : a → ./WListBool → WList) → WList

However, I don't know off the top of my head a more general approach for encoding GADT-style datatypes in System Fw

[zmactep]

And how can WNil and WCons be written for this encoding?

I've tried to use such sort of encoding:

WList = λ(a : *) → ∀(WList : * → *) → ∀(WNil: WList a) → ∀(WCons : a → WList Bool → WList a) → WList a

But by this way I have a problem with WNil type inside WCons definition.

[Gabriella439]

You would first define a WNilBool and WConsBool specialized to WListBool, like this:

$ cat WNilBool
λ(WList : *) → λ(WNil : WList) → λ(WCons : Bool → WList → WList) → WNil
$ cat WConsBool
    λ(x : Bool)
→   λ(xs : ./WNilBool )
→   λ(WList : *)
→   λ(WNil : WList)
→   λ(WCons : Bool → WList → WList)
→   Cons x (xs WList WNil WCons)

... and then define WNil and WCons for the outer type like this

$ cat WNil
λ(a : *) → λ(WList : *) → λ(WNil : WList) → λ(WCons : a → ./WListBool → WList) → WNil
$ cat WCons
    λ(a : *)
→   λ(x : a)
→   λ(xs : ./WListBool )
→   λ(WList : *)
→   λ(WNil : WList)
→   λ(WCons : a → ./WListBool → WList)
→   WCons x xs

[ChristopherKing42]

Something like this would probably work

WList x = ∀ (P : * -> *). (WNil : ∀(a:*). P a) -> (WCons : ∀ (a:*). a -> P Bool -> P a) -> P x

We then get our helper functions like so:

WNil = λx. λ P. λ WNil. λ WCons. (WNil x) WCons e bList = λx. λ P. λ WNil. λ WCons. (WCons x e (bList P WNil WCons))