search

HigherOrderCO / monobook

AGDA
21 stars 5 forks source link

Add a type for lambda terms #5

Open developedby opened 2 weeks ago

developedby commented 2 weeks ago

Create Lam/Type.agda with the type of lambda terms (Lam, App, Var).

Considering that we'll want to have a HOAS evaluator for it in the future it might be interesting to use a type like in Kind-Core https://github.com/HigherOrderCO/kind-core/blob/main/src/Kind/Type.hs, but it can also be a classic concrete encoding that in the future we'll convert to HOAS form when evaluating.

Include a lambda parser based on Data/Parser. Use a similar syntax to hvm1 and bend (λvar bod, (fun arg), var, irrelevant whitespace).

VictorTaelin commented 2 weeks ago

we should indeed have a HOAS type, not a low-order encoding.

perhaps the parser should be a separate issue once this one is done?

developedby commented 2 weeks ago

I separated the parser into another issue, #7