Currently, you have to go (((f a) b) c) where I want it to be f a b c. I'm not very good (or very interested in) parsers, so somebody should have a go at fixing this.

I've intentionally left the propositional equality pretty uninteresting in case anyone wants to play with it. Some open questions:

1. Should it be heterogeneous or homogeneous? The latter might suffice in the presence of equality reflection.
2. I assume the (propositional) equality will be type-directed à la OTT or Nuprl. Other ideas welcome, though!

Quotients

These will be very straightforward. Squashed reflexive-transitive closure of an arbitrary relation.

Binary Unions & Intersections

The binary version of these isn't difficult: for a <= S∪T, either a <= S or a <= T. Likewise, for a <= S∩T, both a <= S and a <= T.

Family Unions & Intersections

It is not immediately clear how to do these in our type theory without making things undecidable. Perhaps an extension to the reflect mechanism...

Dependent Intersections

These will probably be easy. For a <= [x:S]∩T, we just have to check that a <= S and a <= [a/x]T.

Might be interesting to use Arbitrary (from QuickCheck) to generate data that can be used to test the different components and also for benchmarking (e.g., with fixed seeds). It's not completely trivial to do well but the language is probably still small enough that it should be feasible.

• Pair a b should be <a,b> (accepting either fancy angle brackets or plain angle brackets)
• Spread C M p should be spread([p]C; [u,v]M; p). This depends of course of having adjusted the syntax for Split according to #6 first.
• projections for sigmas
• Let

As discussed here: A Type Theory with Scoped Realizability

• Implement a type-directed extraction algorithm
• Replace the equations context w/ a set of in-scope realizers
• Implement the rules from the post
• Change syntax to realize M ||- P in N.

Note: to stop the typechecker from looping, don't check <> <= Id(A; M; N) like in the post. Instead, see if 1 =syn= ExtEq(A; M; N), or if 1 ||- Id(A;M;N) in R. I believe that this will suffice to make typechecking terminate.

Currently we are susceptible to Girard's paradox. This might be a good opportunity to learn how to replicate Sozeau's work on fixing Coq.

It would be nice to add support for named holes. This should be very easy to implement if anyone wants to have a go!

Here's some pseudocode to get you started.

-- Abstract Syntax
| Hole a (Maybe (Ty a))

-- Surface syntax
{?dog} ==> Hole "dog" Nothing

-- Elaborate during checking
check (Hole nm Nothing) t = return (Hole nm (Just t), t)
check h@(Hole nm (Just s)) t = do
  equate s t
  return (h, t)

-- Infer if we've already checked
infer (Hole nm Nothing) = err "Can't infer unelaborated hole or some such"
infer (Hole nm (Just t)) = return t

-- Printing
Hole "dog" (Just t) ==> {?dog : t}

As a bonus, add a pass which finds all the holes in a tree and makes a list of them (optional).

Currently, we're probably normalizing terms lots of times when we don't need to. Might be a good idea to consider a less naïve relationship between check/infer and whnf.

We can't actually extract the bound variable names used in the source, because of the term representation we're using (this is a good thing). But we should generate fresh names rather than just spitting out levels.

• Use some kind of nominal monad: pretty :: Tm -> Fresh Doc.
• Then add back names to the binding syntax λ[x] x instead of λ @1.

We might as well, since we've already paid for it to get Trifecta.

Right now, it's really confusing since we have Id M N S to mean M =S= N. It should be Id S M N.

(Note that the surface syntax is already good. Just the abstract syntax that needs to be changed.)

Need some way to either typecheck a file, or run the REPL. Might be nice to use optparse-applicative, or whatever anyone wants.

Currently, reflection works like this:

  ⊢ (M=N:A) ∈ H
-------------------[hint-projection]
  Γ;H ⊢ M=N:A

  Γ;(H, M=N:A) ⊢ C ⇐ U
  Γ;(H, M=N:A) ⊢ e ⇐ C
  Γ;H ⊢ p ⇐ Id(A; M; N)
-------------------------------[reflection-scope]
  Γ;H ⊢ reflect p in e ⇐ C

Imagine if we had something slightly different. What if the judgmental equality were precisely when propositional equality is trivial:

  Γ;H ⊢ ♦ ⇐ Id(A; M; N)
---------------------------------[trivial-reflection]
  Γ;H ⊢ M=N:A

And the propositional equality Id(A; M; N) is defined by recursion on types, endowing each type with its correct extensional equality. Note that ♦ is the trivial term (called “bullet” in Nuprl), which is synthesizes type 1, but may be checked with that or any true squashed proposition (such as equality).

And then, we would change the reflect construct to not be about equality, but rather to be about bringing the knowledge that a particular term is the computational realizer for another at a particular type into scope. That is, we have a realizability judgment which looks sort of like this: r ⊩ p : S which means that r is the realizer and p is the proof term for a proposition S. Note that the terms of Nuprl are realizers, not proof terms: the proof terms are terms in the logical framework, namely the equality derivations. In general, there is not enough information in realizers for them to be checked against types, but they can always of course be extracted from terms. The computational realizer for any equality is just ♦.

Therefore, the hints box should be reformulated to be a collection of known realizers, and reflect should introduce evidence about realizers into scope so that realizers may be used instead of proof terms. Behold:

  ⊢ (r ⊩ p : S) ∈ H
------------------------- [hint-projection]
  Γ;H ⊢ r ⇐ S

  Γ;(H, r ⊩ p : S) ⊢ C ⇐ U
  Γ;(H, r ⊩ p : S) ⊢ e ⇐ C
  Γ;H ⊢ r ⊩ p ⇐ S
-------------------------------[reflection-scope]
  Γ;H ⊢ reflect p in e ⇐ C

Then, the example we keep bringing up can be given as a special case.

Let P := Id(U; 0; 1).
Let J := ♦ ⊩ p : P.

  ⊢ J ∈ H,J
 -----------------------------------------[hint-proj]
  Γ,p:P; H,J ⊢ ♦ ⇐ P
 -----------------------------------------[triv-reflect]
  Γ,p:P; H,J ⊢ 0=1:U
 -----------------------------------------[1-intro, substitution]
  Γ,p:P; H,J ⊢ ♦ ⇐ 0
 -----------------------------------------[reflect-scope]
  Γ,p:P; H ⊢ reflect p in ♦ ⇐ 0
 -----------------------------------------[Π-intro]
  Γ;H ⊢ λ[p] reflect p in ♦ ⇐ Π[p:P] 0

The moral of this story I'm telling is that we're not building scoped equality reflection, we're building _scoped realizability_.

Comments? @darinmorrison @psygnisfive

A fun way to learn Twelf!

There's a pattern here where I extend a context, peek under a scope, and then rebind the variable, like this:

welp <- extendCtx "x" s $ something (e // V "x")
return $ ("x" \\ welp)

This seems very unsafe, and is causing variables to get renamed which should not. For instance I can check λ[f] λ[x] f ∈ Π[a:Π[a:𝟚] 𝟚] Π[b:𝟚], which is clearly wrong.

I suspect the solution lies in not peeking under the binder like this using substitution & abstraction, but rather somehow getting it so that I can use fromScope and toScope. I just don't know how to do that here...

Thanks to notdan on #nothaskell for noticing this problem.

• Type formation
• Introduction: Pair
• Elimination: Spread
• Also, Spread needs a first parameter which is the motive. So the elimination rule needs to look like this:

     Γ !-[Σ;E] p : Σ[x:A]B             
     Γ, x : Σ[x:A]B !-[Σ;E] C : U
     Γ, u:A, v:[u/x]B !-[Σ;E] M : [<u,v>/x]C
-----------------------------------------------------
     Γ !-[Σ;E] spread([x]C; [u,v]M; p) : [p/x]C

Therefore, we have in the syntax:

Spread :: (B.Scope () Tm a) -> (B.Scope Bool Tm a) -> Tm a -> Tm a

See the wiki for the kind of things I want to add.

The definitional equality is pretty brittle right now. Complications around annotations, free variables, etc. cause havoc.

It would be nice to let things be either checked or inferred... When in checking mode, then _ could be put in instead of a term, and it would be inferred by unification.

Changing the syntax to have maybes in places, and then merging check and infer into one function might be the way. This seems to be the Weirich approach.

• Change Realization to just be a newtype on Tm.

Each declaration should be going into the signature of the environment so that it can be used from future declarations.