Hacker News Reader

Comment by amelius | Hacker News Reader

Question: what would a LISP dialect with static typing look like?

EDIT: Found an answer: http://stackoverflow.com/questions/3323549/is-a-statically-t...

I designed and built a statically-typed F-Expr LISP for my thesis, using some partial AST evaluation to trace and ensure every value had at least an initial value, and from that, type inference.

So it looked like:

    (define fib
      (lambda (n)
        (let loop ((a 0) (b 1) (n n))
          (if (= n 0) a
          (loop b (+ a b) (- n 1)))))

Which would do nothing by itself, and be eliminated as dead code unless called.

If we called it with:

    (fib 10)

It would expand, after the macro stage, to:

    (define fib
      ((Type/Number lambda) ((Type/Number n))
        (let loop (((Type/Number a) 0) ((Type/Number b) 1) (n n))
          (if (= n 0) a
          (loop b (+ a b) (- n 1)))))

If a value couldn't be inferred after ensuring the validity of the AST, it was supposed to error out with some helpful messages, but tracing the entire AST forward and back repeatedly always managed to type every value that was at least initialised, and if not, eliminate it as dead code.

Tradeoffs:

Compiling can be very lengthy, and it would be theoretically possible to write a program that would take ridiculous times to compile.

Once compiled, we can ensure type safety, and in the underlying implementation, JIT everything for a decent amount of speed.

Edit: Forgot to add lambda return type. Then added it in the wrong place.

Do you happen to have a link to your thesis?

Unfortunately not.

I had to surrender publishing rights, and the university only publishes about 10 submissions a yeaar... So unlikely to appear anytime soon.

> I had to surrender publishing rights

Even as a pdf on your own webpage? What kind of university would do that? Even the most abusive CS publishers have a more relaxed policy…

Well, the nearest competitor requires full copyright transfer, so there's that.

And CS publishing usually happens only within STEM, not as a standalone, within this circle of Universities.

No, not in America. There is far less interest locally in CS, and so a sort of mild tyranny rules in academia.

Common Lisp, Racket, and Clojure all have optional static typing.

They have gradual typing but I believe they're still enforced as runtime contracts, making them not static types.

In a Typed Racket program that does not import any untyped racket code, there is no runtime enforcement. Runtime contracts are only introduced at the boundary between typed and untyped code. This allows programs to be soundly transitioned from untyped to partially typed to fully typed.

That sounds pretty rad. Do you know what the status is of dependent types in Racket? I have always been interested in that.

We're working on it! See the work by my student, Andrew Kent, coming soon to Typed Racket: https://pnwamk.github.io/

Technically, the Common Lisp standard leaves it up to the implementation what to do with type declarations--in practice, I get compile time warnings for violating them (as well as for violating inferred types). Type declarations will not lead to runtime checks, you need to use CHECK-TYPE or similar for that.

Typed Racket is more extensive and gives errors at compile time. I don't know very much about how it works in Clojure.

In SBCL, type declarations are treated as assertions. If the compiler is sure the assertion is valid without doing runtime checks, it can remove them. The optimization levels are also taken into account (http://www.sbcl.org/manual/index.html#Handling-of-Types).

http://www.shenlanguage.org/

Here's my attempt:

https://github.com/burtonsamograd/typed-cl

Dylan.

Reply on news.ycombinator.com