Stlc theory

[jake-87]

Description

Added a very simple STLC, alongside several properties. Still WIP.

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

[Lavenza]

Pull request preview

New pages

• Lang.STLC.Named (+742, -0)
• Lang.STLC.DebruExtrinsic (+431, -0)
• Lang.STLC.DebruIntrinsic (+277, -0)

Changed pages

• Data.Fin.Base (+6, -5)

[jake-87]

I'm going to not push anything up here for a little bit while I work on the substitution problem; I feel like it's going to be quite messy while I figure it all out.

[jake-87]

Sorry about the slightly sloppy commits, I'm happy to squash them before any of this is merged.
Still very much a WIP.

[jake-87]

I'm going to tentatively open this up to review. Currently does not include strong normalization & related, as discussed on the Discord.
Also needs a base page that links to the three.
@TOTBWF Would especially appreciate your input, if/when you have the time :)

[TOTBWF]

I've been looking forward to this PR for a while, glad to see it's ready to review 🥳

I'm going to split my review into a couple of rounds to avoid burying you in a mountain of requested changes. First pass is style stuff in Lang.STLC.Named.

Some general notes:

• We might want to consider some variable blocks for things like contexts: this could shorten a lot of type signatures.
• We might want to consider a Data.List.Snoc with some pattern-fu to make goals always show up as snoc rather than cons, along with some re-exports of flipped append and the like. Alternatively, we can Uphold Snoc List Thought and just have Data.Bwd as a bona-fide data type. Not sure about the best design here, @ncfavier @plt-amy thoughts?

Finally, are you okay with me making edits to the PR directly? If so, I could do a formatting pass myself to save you the trouble. However, if you want to do it yourself to get a better feel for the style guide, that's totally fine by me 🙂

[jake-87]

I'll ping again this is ready for review again (once all suggestions are fixed, and I've fixed some stuff I've personally noted)

[plt-amy]

Do we need this when we have https://1lab.dev/Cat.CartesianClosed.Free.Lambda.html?

[jake-87]

Perhaps not? That page takes a much more evaluation-centric view, so it might still be nice to have a reduction-centric view around somewhere though.

[jake-87]

This is ready for a proper review again, now (page: @TOTBWF). I believe most everything has been addressed nix ongoing discussion points? (and CBV, but I have some larger ideas there that can perhaps wait)

Also: Formatting is still being worked on, so don't worry about that, and I'll push something to fix the build when I get the chance.