Article Accepted for ELS 2021: A Portable, Simple, Embeddable Type System

We are happy to announce that our paper has been accepted for presentation at the 2021 European Lisp Symposium.

A Portable, Simple, Embeddable Type System

We present a simple type system inspired by that of Common Lisp. The type system is intended to be embedded into a host language and accepts certain fundamental types from that language as axiomatically given. The type calculus provided in the type system is capable of expressing union, intersection, and complement types, as well as membership, subtype, disjoint, and habitation checks. We present a theoretical foundation and two sample implementations, one in Clojure and one in Scala.

7 Likes

@Jim_Newton Is the sample implementation for Clojure open source and can we try it?

try this out Jim Newton / clojure-rte · GitLab

5 Likes

Congrats!
I’ve been meaning to ask you, have you had a chance to look at this work?

1 Like

No, but that’s a very interesting project. It is indeed similar to my work. Why haven’t I found an academic peer-reviewed published article about it?BTW I sent the author an invite on LinkedIn, to chat about his work.

1 Like

Perhaps one reason for the lack of publications is that when you understand the concept, it is very intuitive. However, the theoretical foundation is subtle. That’s what I hope to explain in an upcoming article. The basic theoretical problem is that finite automata work on FINITE alphabets. but the set of objects in a programming language is infinite and the set of types is the size of the power set of that infinite set. thus the fundamental assumption of finite automata theory is immediately violated.

Nevertheless, it still works. why? and what are the limits? That’s the theoretically interesting part.

2 Likes

I think you’ve seen no publications on the subject because Metosin weren’t approaching the problem from a formal, rigorous direction, but a practical one.
I think Malli could be said to have a finite alphabet as well, which is its registry, not every object in the language. The registry is defined for the objects used in Clojure, everything else and the program will terminate abnormally.
Interestingly, you can extend the registry (i.e. the alphabet)

2 Likes

Here’s a link to the draft of the 13 minute demo part of my ELS talk.
I welcome anyone’s feedback while there’s still time to change the video.

3 Likes

That’s neat. Is there any way with genus to type maps in a row polymorphic style? Or maybe a structural subtyping style?

Something like:

(dsfn foo
 ([{:keys [^Int bar]}]
  (list 'int 'bar bar))
 ([{:keys [^Int baz]}]
  (list 'int 'baz baz))
 ([{:keys [^String bar]}]
  (list 'string 'bar bar)))

I think the answer is yes. The docs for genus specify how to add new types. In doing, you must specify how to compute the subtype and disjoint relation to all other types, which may always be dont-know.

@didibus, can you help me understand what kind of call-site argument list can be applied to a lambda list such as [{Keys [bar]}]? 1) what does the programmer expect, and 2) what does the language allow. For example, can a key named :bar be given multiple times, or exactly once, or at least once? If multiple times, which one is bound to the variable bar ? Are they all expected to be the indicated type, or only the first or only the last expected to be of the specified type? Is the designator expected to be a symbol such as bar or a keyword such as :bar?
Are other unmentioned keys allowed or not?

These types of specifications are very well stated in the case of Common Lisp, and I know them well, but I don’t know the rules for Clojure

I was trying to find an explanation of how binding is done in function application. I looked in the closure reference page but don’t find anything. I.e., what are the rules of what the call-site argument list can look like and what the function definition argument list (the lambda list) can look like. Does anyone know where it is documented?