Rambling about TTF and Drasil Chunk Building

[balacij]

One of the really nice things about TTF is that we "say something" without really
committing what we said to being of a particular class of similar things said, and
we can grow expressions, limiting what things it can possible evaluate to. One
of the nice things about it is that once we've committed it to a particular thing,
the thing we committed to it has a type, and that type is our finalized "type" of
the thing we constructed.

I think this is a very powerful concept about assigning meaning to words according
to context.

Now, let's think about Drasil w.r.t. chunk building. Right now, we build chunks as
matryoshka dolls, gradually building up a hierarchy of chunks that slowly build up
to a whole "thing." One of the issues with this approach is that we don't really
have any information about what the "maximal chunk type" is of any particular
"thing." However, we do know what the capabilities are of any particular "thing."
By observing the series of tables in the chunk database, we can accurately tell
you everything we know about any "thing" and form some general idea about what we
can do for you, but we don't really capture its final type.

(I know I've had issues with the gradual chunk building in the past, but that's
not to say that I'm against it, at all. Rather, I think there might be something
we can reconcile by embracing TTF ideology somehow because I'm a bit skeptical
that doing a 180 into a "flat" chunk structure will cure everything [and I think
we've discussed that it wouldn't be either].)

Anyways, thinking about Drasils chunk building, we attach features when we
gradually build chunks. At times, we might attach features in diverging directions
and split up a "base chunk" into separate chunks, but that's not really an issue
because we should be ending up with different UIDs too [Note: this is actually
an issue with the current gradual style, we manually assign a UID very early on].

Now, if we were to move away from the matroyshka-style chunk building, I think it
would be nice to build chunks with the same style as TTF does for expressions,
and have the final type be something that we resolve through the description of
the features that we described when forming a chunk. By doing this, when we build
chunks:

1. if we have an idea of what chunk type we want to build, then we know what terms
   we need to attach to the chunk
2. if we don't know what type of chunk we want to build yet, we can potentially
   have Drasil resolve the type for us (e.g., through similar magic to TTF), or
   we can find out that we might need to build a new type to describe the thing
   we want to build

When I talk about features, I mean features that we describe through the current
type-classes we build up.

One of the features of TTF that we might want to avoid is having ambiguous types
that we can resolve to for any particular expression. In other words, we would
be describing our chunk types through a series of features (type-classes) and
saying that that specific structure of features is a unique "type." Now, of
course, this might not at all be possible in Haskell because we can't enforce
that any particular mixture of type-classes must resolve to at most one type.
Thus, this might mean that we need some sort of DSL that runs at the TH-level,
or that we need to embrace de-embedding Drasil and using Haskell as an interpreter
for an external "Drasil chunk specification language." Implementation-wise,
there's still many things to think about.

The nice thing about building chunks in this way is that we still get gradual
chunk building, but the chunk structure is also flat. So we, in some sense, get
the best of both worlds.

[balacij]

I'm not too sure everything fully makes sense, or is explained well enough, but I think there might be something we can learn from TTF-style interpretation resolution in Drasil, when we build chunks. This is, of course, heavily relevant to #2873, #3003, #3134, and #2911.

To be clear, I know the original post is missing a lot of information and jumps around, but I wanted to write something down before I forgot it. If it doesn't resonate with anyone yet, then I will try to re-write it later, after finishing my thesis.

[smiths]

I probably should know this already, but what is TTF-style?

[balacij]

Ah, TTF is the "tagless-final"/"typed tagless"/"typed tagless final" style of building DSLs. I refer to it as "TTF" because the first paper @JacquesCarette introduced us to in CAS 761 referred to it as the "typed tagless final".

[balacij]

Random thought I wanted to get down: theory presentations and TTF. What are the relationships?

[JacquesCarette]

TTF is a way to embed one language into another, in such a way as to be 'representation polymorphic'. As theories presentations are a form of language, one can use such a representation.

TTF is most useful when you want to write multiple interpreters for the same language. Otherwise it's overkill.

[balacij]

Thank you, @JacquesCarette!

Now, out of curiosity, can we re-create TTF using theory definition modules? I can vaguely see it, but I don't know if I can see any benefit.

Also, if we had languages represented in theory definition modules and use theory extensions, can we also similarly “answer” the expression problem? I imagine this would be good in the cases where we want pattern matching on the TTF language (e.g., in the case of Expr/ModelExpr/CodeExpr) but want to avoid the Haskell (G)ADT boilerplate associated (or that of any other language). I mean, wouldn't using theory definitions, extensions, etc. simplify building languages with the expectation that they would be extended in various ways?

[JacquesCarette]

You can, by being abstract over a constructor, something of "type" type -> type. But the rest is all "open", in the sense that no one's done anything like it before. It all feels quite doable, but there might be various things that get in the way, in practice.

I've been meaning to write a "finally tagless" paper but in Agda. Maybe once your courses are over.