The generic-reuse from larrytheliquid

generic-reuse's People

Contributors

Stargazers

Watchers

generic-reuse's Issues

change x-vs-y naming convention for fix combinators

Also change it in the examples, and in the Tex.
Currently x and xs are used, when sometimes y and ys makes more sense.

Also update index-index branch.

Difference between definition of AssocV in paper vs code

In the paper, AssocV is defined very concisely:

AssocV ◂ AppV → ★ = λ appV.
∀ A : ★. ∀ n : Nat. Π xs : Vec A n.
∀ m : Nat. Π ys : Vec A m. ∀ o : Nat. Π zs : Vec A o.
appV (appV xs ys) zs ≃ appV xs (appV ys zs)).

In the code, however, it depends on four auxiliary definitions:

AssocV4 ◂ AppV ➔ Π A : ★.
Π n : Nat. Vec · A n ➔ Π m : Nat. Vec · A m ➔ Π o : Nat. Vec · A o ➔ ★ =
  λ appV : AppV. λ A : ★. λ n : Nat. λ xs : Vec · A n.
  λ m : Nat. λ ys : Vec · A m. λ o : Nat. λ zs : Vec · A o.
  {appV (appV xs ys) zs ≃ appV xs (appV ys zs)}.
AssocV3 ◂ AppV ➔ Π A : ★. Π n : Nat. Vec · A n ➔ Π m : Nat. Vec · A m ➔ ★ =
  λ appV : AppV. λ A : ★. λ n : Nat. λ xs : Vec · A n. λ m : Nat. λ ys : Vec · A m.
  ∀ o : Nat. Π zs : Vec · A o. AssocV4 appV · A n xs m ys o zs.
AssocV2 ◂ AppV ➔ Π A : ★. Π n : Nat. Vec · A n ➔ ★ =
  λ appV : AppV. λ A : ★. λ n : Nat. λ xs : Vec · A n.
  ∀ m : Nat. Π ys : Vec · A m. AssocV3 appV · A n xs m ys.
AssocV1 ◂ AppV ➔ ★ ➔ ★ = λ appV : AppV. λ A : ★.
  ∀ n : Nat. Π xs : Vec · A n. AssocV2 appV · A n xs.
AssocV ◂ AppV ➔ ★ = λ appV : AppV. ∀ A : ★. AssocV1 appV · A.

Is this because the version in the code is more generic than the one in the paper, or are these four auxiliary definitions strictly necessary to make it work? Also, could you share some intuition on what they're good for?

Add the non-dependent folds for the Base types.

How can I typecheck these examples?

Is there a typechecker which can verify all these examples? Is it this one: https://github.com/MaiaVictor/cedille-core ? If yes, how can I use it? A few lines about this in the README would be appreciated 😉

Recommend Projects