Dana needs a self-embedding of U-Box

My first major goal in Dana is to write a console session interpreter, in which you can construct, name, compose, and observe Dana objects in the console. Since this is a foundational project, I best say what it is I mean by “console session”:

    newtype ConsoleSession = ConsoleSession (String -> (String, ConsoleSession))

In layman’s terms: a console session is a stateful function from input lines to output lines. Then the “hardware” will observe this by allowing you to type things in the console and showing you what the function returned.

Let’s say that this console session has a dictionary from strings to values and their types, and the user tries to apply one of those values to another. This might be illegal, since the types might not match up. Everything has to be well-typed, so we can’t just “try it and see”. If the Type of types is exposed (I’m not sure if it should be — it’s a question of whether the class of types is extensible), it looks like this:

    data Type where
        Type :: Type
        Pi :: (x:Type) -> (x -> Type) -> Type
        ...

With some other stuff — those are the two most important. Notice that Pi has a function in it, so we cannot compare two Types while maintaining referential transparency and functional extensionality. These properties are very dear to me, so Dana had better have them too!

So how can we tell whether this application is well-typed? It doesn’t suffice to keep the types themselves in our dictionary; we need to keep quotations of them with decidable equality. I.e. we have to have:

    TypeRep : Type
    embed : TypeRep -> Type
    equal : TypeRep -> TypeRep -> Bool

But then, when it is well-typed, we need to actually perform the application, which we can only do if it’s well typed. Bool is not a good enough return type for equal:

    equal : (x:TypeRep) -> (y:TypeRep) -> Eq Type (embed x) (embed y)

Where Eq is the usual:

    Eq : (A:Type) -> A -> A -> Type
    Eq A x y = (P : A -> Type) -> P x -> P y

Then, if libraries wish to be accessed via the user, they should export TypeReps for every Type they export. For example:

    Export : Type -> Type
    Export T = (rep : TypeRep ; Eq Type (embed rep) T)

    Integer : Type
    IntQuote : Export Integer

I suspect that such a quotation scheme will be quite a challenge to create (it also corresponds to U-Box proving its own consistency, thus U-Box is inconsistent — but we already knew that :-). It could be fun to attempt if I’m in the mood for tricky mathematics. If I’m not in such a mood, I guess I could also cheat and provide TypeRep, embed, and equal as primitives, which might be the way to go just to get things rolling.

The necessity of quotation is the main reason that the core U-Box calculus should be as simple as possible, and most of my effort in this early stage should go toward simplifying it. Is there a combinator calculus for dependent types? That would make things easier.

About these ads