Earlier quoted context omitted.
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
Awesome! Nice find.
Type Systems as Macros
11–17 of 17 posts
Re: Type Systems as Macros
#12Can this be used to type check the language used for macro generation too? Like could this be used to implement a typed racket?
Re: Type Systems as Macros
#13How powerful is the type system? Can you do dependent types?
Re: Type Systems as Macros
#14How powerful is the type system? Can you do dependent types?
> Can you do dependent types?
Yes. For example, see https://github.com/wilbowma/cur
Re: Type Systems as Macros
#15Doesn't Typed Racket work on the same basis?
Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then typechecks the core language.
Our approach uses macro expansion to typecheck the surface language and translates it into an untyped core language.
The two approaches should be considered alternative tools in a programmer's toolbox.
Re: Type Systems as Macros
#16Can this be used to type check the language used for macro generation too? Like could this be used to implement a typed racket?
It could, though it's not clear whether it would be an improvement.
Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then type checks that core language.
This approach works well because the surface and core languages are similar, and thus the type checker need only handle a small number of core forms.
This approach is limited, however, to constructs that are translatable into the core typed language. For example, a few Racket `for/X` comprehension forms are not supported in Typed Racket because they are difficult to translate.
Our approach alternatively uses macro expansion to type check the surface language and translates it into an untyped core language. Thus it's less limited in the typed languages one may implement. The tradeoff is that the programmer must implement type rules for all forms in the surface language, rather than just the core language.
Re: Type Systems as Macros
#17I'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
Awesome! Would love to check it out once you have a prototype.