msp-strath / typos Goto Github PK

There are a number of types (like MachineStep in Options) that have both Show and Pretty instances. Is this on purpose?

https://www.youtube.com/watch?v=2ZmoexvTw6c

Mostly just recording this here so we don't forget it, and because it is always satisfying to close issues: after Monday's increase in static analysis, which necessitated an increase in intention in the source language (e.g. declaring the syntactic categories of stashes, and fresh metavariables), the examples in the README are currently out of date with reality.

TypOS has a very simple raw syntax: pairs and atoms, bindings and variables, metavariable instantiations. We could just use raw terms for everything, but that offers considerable potential for subtle errors. I propose that we equip ourselves with the means to characterise sets of raw terms which are in some sense well formed. E.g., we might introduce the distinction between "checkable constructions" and "synthesizable computations". Thus equipped, we can say which sorts of thing go where in judgement forms.

What are syntaxes like? As a syntax designer, I should be able to

1. Name syntaxes, and recursively demand substructures of a given syntax.
2. Demand a pair whose head has one syntax and whose tail has another, depending on the head.
3. Demand the nil atom.
4. Demand a binder, specifying the syntax of the bound variable and the syntax of the term under the binder.
5. Demand one of a specific set of non-nil atoms.
6. Perform case analysis on a component of known syntax, in order to compute a syntax.

I thus have to say what patterns are like. Note the "Law of Explicit Discrimination": the only things we can tell apart are non-nil atoms.

We could go nuts and define something an awful lot like type theory.

Let's at least try to spend fewer bucks, as long as we get enough bang.

Sadly this line

https://github.com/msp-strath/TypOS/blob/main/Src/Actor.hs#L125

is not doing the right thing in general: in our stlctpp.act example, we have scopeEnv env = 1 and sc = 3 when mangling the term before we send it, resulting in a thinning of size -2... What is fun is that versions of GHC < 9.0 silently truncates our use of shiftL to 0, whereas newer GHC versions crashes with an arithmetic overflow.