Dependent Type Systems as Macros [pdf] | Hacker News Reader

Dependent Type Systems as Macros [pdf]

williamjbowman.com

95 pointsluu7 comments

Open articleView on HN

It's nice to see the work from Type Systems as Macros (also Stephen Chang of NU) continued! Thanks for sharing.

http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf

Thanks for the comment!

The submitted link might be an older preprint.

Here is the official acm link to the paper: https://dl.acm.org/doi/10.1145/3371071

So a type system using macros, I assume this would enforce types at compile time and not runtime? I don't really see the value of type checking at runtime; I won't catch type errors until after the system is deployed! Would like to hear others opinions because people are really excited about clojure.spec. I just feel like it adds additional overhead for... slightly improved error messages? I could see the value in a type system for Lisps/Clojure that happens at compile time, it's very helpful in Haskell.

Something like spec in Clojure can be used for something like validations; you have basically a full context-free-grammar syntax to play with (sort of disguised as a type-system) that makes validations (in my opinion) a lot simpler than trying to do your own regex-and-split glue. You can use it to validate web forms, or just for sanity-checking data.

Since most people write some level of unit-testing for Clojure anyway, adding spec type-signature functions gives you something like a compile-time typecheck that is relatively easy to add to your CI or simply by invoking `lein test`. In combination with generative testing, being able to have a CFG system to use for your types ends up being a lot more powerful than Hindley-Milner, closer to a dependently-typed system.

Also, while I'm reasonably certain that spec doesn't do this, it's not unreasonable to think that a runtime type system could be used for optimizations that can't be fully known during compile-time.

Yeah, macros are expanded as part of compilation in lisps.

However, lisps blur the distinction between run-time and compile-time somewhat because you usually connect your development environment to a running system while developing (it’s somewhat like using a debugger in other languages.) and I, at least, develop the initial version of a new function in the REPL before copying it into my source code, generalizing it and writing tests: so, for the most part, I will see the runtime type errors during development just as if I had been using a compiler/IDE to check the types.

Correct. More specifically, type checking is performed as part of macro expansion, which happens at compile-time.

Reply on news.ycombinator.com