Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Dependent Type Systems as Macros [pdf]

williamjbowman.com

Post reply on HN
Print view View original

1–8 of 8 posts

Re: Dependent Type Systems as Macros [pdf]

#3

Post by j_m_b »

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.

Re: Dependent Type Systems as Macros [pdf]

#4

Post by tombert »

j_m_b wrote: post #3

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…

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.

Re: Dependent Type Systems as Macros [pdf]

#5

Post by fiddlerwoaroof »

j_m_b wrote: post #3

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…

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.

Re: Dependent Type Systems as Macros [pdf]

#8

Post by stchang »

j_m_b wrote: post #3

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…

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