~ashton314/understanding-turnstile

b5720920b729cce7453847d6d58b672855f3e35f — Ashton Wiersdorf 1 year, 1 month ago 64aed33
Add license and README
3 files changed, 34 insertions(+), 0 deletions(-)

A LICENSE
A README.md
M play_stlc.rkt
A LICENSE => LICENSE +9 -0
@@ 0,0 1,9 @@
MIT License

Copyright © 2023 Ashton Wiersdorf

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice (including the next paragraph) shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

A README.md => README.md +22 -0
@@ 0,0 1,22 @@
# Understanding Turnstile

Turnstile is a system for developing typed DSLs using macros in [Racket](https://racket-lang.org), and was introduced in the paper *Type Systems as Macros*. [<a href="#citeproc_bib_item_1">1</a>] It's a fascinating idea, but the paper is a little difficult to follow. This repository implements the basics of a type system with macros using straight-forward Racket, and takes up only 68 lines in a single file. (`stlc.rkt`)

I have a write-up about this [on my blog](https://lambdaland.org/posts/2023-08-14_types_with_macros/), which I recommend reading if you're new to this.

## License

MIT.

## Authors

 - [Ashton Wiersdorf](https://lambdaland.org/) (just this particular implementation, not the paper from which the original idea came)

## References

<style>.csl-left-margin{float: left; padding-right: 0em;}
 .csl-right-inline{margin: 0 0 0 1em;}</style><div class="csl-bib-body">
  <div class="csl-entry"><a id="citeproc_bib_item_1"></a>
    <div class="csl-left-margin">[1]</div><div class="csl-right-inline">Chang, S., Knauth, A. and Greenman, B. 2017. <a href="https://doi.org/10.1145/3009837.3009886">Type systems as macros</a>. <i>Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages - POPL 2017</i> (Paris, France, 2017), 694–705.</div>
  </div>
</div>

M play_stlc.rkt => play_stlc.rkt +3 -0
@@ 11,3 11,6 @@

;; an example of an ill-typed expression
;; ((λ ([x : (→ b b)]) x) (λ ([f : (→ b c)] [y : b]) (f y)))

;; another
;; (λ ([f : (→ a b)] [x : c]) (f x))  ; x is the wrong type!