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

Type Systems as Macros

lambda-the-ultimate.org

Post reply on HN
Print view View original

1–10 of 17 posts

Re: Type Systems as Macros

#3

Post by naasking »

moomin wrote: post #2

Doesn't Typed Racket work on the same basis?

This is a little more general. They implement a stack of type systems all the way up to F-omega, and they're able reuse and compose the macro libraries to make the more elaborate type checkers. It's pretty impressive.

Re: Type Systems as Macros

#5

Post by chriswarbo »

LightMachine wrote: post #4

eli5?

Macros are run at compile time, and are used to rewrite source code prior to interpretation or compilation. They're mostly used to make nicer syntax, e.g. a macro could turn an expression like `(with-file (f "/tmp/foo") ...)` into a working implementation like:

    (let* ((f (open "/tmp/foo"))
           (result ...))
      (close f)
      result)
Here, the authors make macros for type annotations, i.e. they take expressions like `(my-value : my-type)`, check whether the types unify correctly, and spit out an untyped expression implementing that value if they do.

By using macros, the type system becomes modular: new type system features (subtyping, kinds, etc.) can be written by the programmer as a set of macros, rather than as a whole new language (and all of the work that entails). They test their claim by implementing a bunch of features, combining/reusing them in a bunch of mini languages, and write some semi-plausible programs in these languages, to see if they're realistic.

Re: Type Systems as Macros

#6

Post by notjack »

moomin wrote: post #2

Doesn't Typed Racket work on the same basis?

Typed Racket runs after macro expansion, performing analysis on fully-expanded code. This technique runs as part of macro expansion, rather than after. The upshot is that macros get to use and generate type information, so language and type system features like typeclasses or GADTs can be library-provided macros.

Re: Type Systems as Macros

#7

Post by chombier »

This is beautiful. I especially like how the type environments naturally arise from lexical scope during macro expansion.

The fact that this composes all the way up from simply typed lambda-calculus to F-omega is pretty impressive.

Re: Type Systems as Macros

#8

Post by moomin »

naasking wrote: post #3
moomin wrote: post #2

Doesn't Typed Racket work on the same basis?

This is a little more general. They implement a stack of type systems all the way up to F-omega, and they're able reuse and compose the macro libraries to make the more elaborate type checkers. It's pretty impressive.

Ok, that is rather cool. Could something like this be used to make a better Template Haskell?

Re: Type Systems as Macros

#9

Post by nonsince »

moomin wrote: post #8
naasking wrote: post #3

Earlier quoted context omitted.

This is a little more general. They implement a stack of type systems all the way up to F-omega, and they're able reuse and compose the macro libraries to make the more elaborate type checkers. It's pretty impressive.

Ok, that is rather cool. Could something like this be used to make a better Template Haskell?

Someone's working on something like that already https://github.com/lexi-lambda/hackett

Re: Type Systems as Macros

#10

Post by nonsince »

I'm glad this has shown up here, I discovered it very shortly after publication and it completely overhauled the way I thought about language design. I'm currently intermittently working on a language based on this concept, as an environment to create languages that compile to LLVM bytecode to complement Racket's environment to create languages that compile to untyped lambda calculus
Post reply on HN