Prolog Über Typing -- clp(type) ??

[jjtolton]

I'm looking for help with clarifying terminology on a category of problems that seem to relate to Prolog meta-interpreter work. I am interested in demonstrating how Prolog can be used for interesting type system work. (Note: that I am not suggesting the introduction of static types to Prolog, what I mean is that Prolog can be used to verify interesting properties of programs meant to be interpreted via meta-interpretation.)

The beauty of a meta-interpreter is that it can take the same code and execute it in a number of different ways. However, generally you cannot splice together meta-interpreters and expect them to work coherently.

Problem one: Type constraints

To make the example more concrete, let's say I have some code C that represents a user interface. Let's say I have a set of meta-interpreters that generate code suitable to translate C into React, vanilla JavaScript, or HTML5 canvas. Each of these would have the same set of features -- buttons, menus, tables, etc, which are all semantically encoded in C.

Now let us focus in on the type of a button in C. It is clear that the type of button cannot be considered in isolation. HTML5 canvas and React are for the most part incompatible user interface technologies, and I believe that any effort to make these two technologies work together in a general manner would be needlessly convoluted. (regardless of whether or not you believe this statement to be true, I request that we accept as a premise that there exist a set of components components(A) and components(B) where A and B are internally coherent but not interchangeable with the other)

Going back to the button, again it seems clear to me that the type of button -- the type of button seems to depend on the type of all the other components in the set -- those that would be naturally generated by an internally consistent meta-interpreter. So once the type of button is constrained by the choice of concrete type by another component, then we can know the concrete type of the button.

However it is also clear that button is a distinct thing from table, so it is not the case that button can just be ANY type. At the very least it needs to be mutually exclusive from table.

Problem two: descriptive or semantic typing

I am not sure that this problem is even a computable problem and not an aesthetic problem, but it is fairly clear (to me, anyway) that a table is not a button. Even if we solve Problem 1, and we have a language that says "the type of button depends on the type of table" and vice versa, this does not necessarily solve the problem of a button must satisfy the semantic properties of button in all incarnations of button and a table must satisfy all semantic properties of a table for all manifestations of table.

In other words, what would make me certain that the React version of a table and the Canvas version of a table would both have a title, rows, and columns? Or that a button is clickable? It seems like we must do more than simply "tag" a button as a "button" and a table as a "table".

Here is another perhaps more concrete example -- if you are sending an HTTP Request, the final output might be a string or bytes. But it is clear that not ANY string or bytes will do -- it must be compliant with with the RFC standards for HTTP requests. This is a much more specific constraint that string or bytes.

Problem three: type dependencies

The simplest version of this I can think of is foo(A,B), but there is a constraint that A must be an integer and less than B. We could of course check this at run time but that doesn't let us reason about the properties of the program itself.

Or imagine a pair of functions, foo(A,B) and bar(X,Y). We could imagine a more complex set of dependencies, but to keep it simple we could say that A < B if X < Y (or variations on that them).

Recap:

I am sure someone has probably thought of these problems before, and it has probably even been done in Prolog. But these are all just vague, fuzzy, imprecise observations problems I have run into and I would love some more formal terminology on these things if anyone has knowledge of them.

So I suppose the three categories of problems I'm curious about:

• "type system constraint programming" or "types of type systems" or Über Typing I guess?
• semantic typing?
• predicative dependencies between types, both near and long-range?

I realize this is very vague, it has taken me awhile just to formulate the question. If anyone has any leads on resources, I would be quite appreciative!

[haijinSk]

[jjtolton]

This is quite interesting. I had not considered that this could be viewed as a graph theory problem, and that the resolution to the type dependencies could be related to the path through the graph. 🤔

[jjtolton]

Wow this is quite bold! I did not know you were "allowed" to do this, it's so powerful it seems like cheating! 😮

[jjtolton]

Wow this is quite bold! I did not know you were "allowed" to do this, it's so powerful it seems like cheating! 😮

I think, it is powerful when we can check so many things (encode with types what we really mean) about our program before we run it. Yes, static types could be "fancy", but I would rather "use" a car, aircraft, or a medical device programmed with dependent types than without...

Yes indeed. The thing with Prolog is that the combination of meta-interpreters + DCGs makes it an ideal transpiler language. So if I have the semantic concept of a "user", I should be able to generate database code, front end code, back end code, testing code, and infrastructure code related to the semantic concept of "user". Even though they are in different languages and possibly completely different type systems and paradigms, it seems like using something like "dependent types", you should be able to make sure that certain properties for "users" hold in all target representations of the concept.

[hurufu]

There is already Hindley-Milner type system implemented for SWI: https://www.swi-prolog.org/pack/list?p=type_check, we can port it to Scryer.

[jjtolton]

Thanks! I was looking for a Prolog implementation of Hindley-Milner!

[hurufu]

Just want to step back, and appreciate Prolog – do you know a lot of languages where it is possible to implement whole type system as a library and blend it seamlessly to the core language? I think this is really a unique feature not matched by any language (even Lisp) with the same sort of elegance.

[jjtolton]

Absolutely. Wouldn't even attempt this or be able to conceptualize it in another language.

[mthom]

@jjtolton , a lot of what you're describing sounds like dependent types. I scroll down and see you're looking at Idris. That's the right track to be on.

Seems as good a time as any to remind people of my own whack at this topic: https://github.com/mthom/scryer-shen

I'm rewriting the Lisp side of the system in Common Lisp. Racket is a nicer and more elegant language than CL in many respects but I found I couldn't quite push it in the direction I want to go. The most ambitious is a stepwise proof tree visualizer allowing the user to pinpoint exactly where a proof went wrong (or right) in nicely rendered typography. The most opaque part of Shen is probably its very powerful but opaque type search process.