Template Dhall?

#1

Several things recently gelled in my mind, after

Generally, there sure seems a lot of demand for extensions to the language of a particular type. Each extension is generally type-safe, and if it could be simply added to Prelude nobody would bat an eye. The trouble is that they can’t be expressed in Dhall: they cannot even be given a Dhall type. That means each construct has to be added to the language specification, and then to every single implementation. That’s a heavy burden to impose.

My first problem formulation attempt called these things language plugins, but that doesn’t help implementors.

Then finally it hit me that many of these extensions could be implementable if we allowed them to operate at meta level, if they were functions on reflections of Dhall expressions. So for example while toMap doesn’t have a type, at the meta level it would be a function from a reflected record to a reflected list. A reflected record is just a list of reflected fields, and a field is a record of field name and reflected type. Generally speaking, a meta-level function could be given a type of

let MetaFunction = MetaExpression → < result : MetaExpression
                                    | next : MetaFunction
                                    | error : Text >

When a MetaFunction is pulled into scope — which could be restricted to file or Prelude imports only — its argument would be automatically converted to a MetaExpression, then the function would be applied, and if successful the result would be reified back to a surface-level Dhall expression.

I see the main benefit of this approach as shifting the implementation burden from the host language implementations to Prelude. The implementations would need to implement the meta-language support only once, and then fromMap, toMap, merge, and many more untypeable constructs could be implemented in Prelude for everybody’s use. Depending on how Text values gets reified, other constructs like toJSON could also be automatically covered.

Now of course the downside of this idea is that it would permit heretofore unpermissible things, so it would lower the security guarantees. I think if we can restrict it to Prelude alone that is not a problem, but @Gabriel439 may feel differently.

#2

@blamario: I think the issue you’d run into is that Dhall isn’t sufficiently powerful to describe manipulations of its own AST because of the restrictions on recursion. There are some things you’d be able to do but in general you’d probably run into the limitations of the language.

For example, one of the things you’d need is to be able to β-normalize terms before pattern matching on the term, but we can’t encode β-normalization in Dhall.

#3

I think the issue you’d run into is that Dhall isn’t sufficiently powerful to describe manipulations of its own AST because of the restrictions on recursion. There are some things you’d be able to do but in general you’d probably run into the limitations of the language.

I’m aware of that. In case of toMap, for example, we’d want to ensure that the record is monomorphic which would at least require an equality check on the reflected types. My question is whether this route is worth investigating at all. I could expand on the design if it is.

For example, one of the things you’d need is to be able to β-normalize terms before pattern matching on the term, but we can’t encode β-normalization in Dhall.

I was assuming the argument expression would be first fully normalized and then reflected. I don’t know what should be done about lambdas. I suppose the reflection could use DeBruijn indexes. Anyway, we could restrict the arguments to ground terms to start with. Of the possible uses I have in mind only one would allow a function argument, and that one is probably hopelessly complex. It’s Grammar/fix I mentioned elsewhere.