5 ms·
For programming languages, dependent types. DT is a hot topic in the PL community recently. It massively enhances the capability of a type system by turning it
by juxtapose 5y ago
For programming languages, dependent types.
DT is a hot topic in the PL community recently. It massively enhances the capability of a type system by turning it into a comprehensive logic system, so you can encode whatever properties you'd like to enforce into a type signature. Theorem provers have been taking advantage of the Curry-Howard correspondence for some time, but the implication of DT on real-world programming is still not well understood (we need more real-world projects written in DT languages). There are also ambitious projects that want to bring DT into the mainstream.
If you are interested, you can take a look at Lean [1], Idris [2], and a few others [3,4]. Often these languages have esoteric syntax, but there are projects using a more conventional syntax, too, e.g. Cicada [5]. "The Little Typer" [6] is a pretty good introduction to this topic.
[1] https://leanprover.github.io https://leanprover.github.io
[2] https://www.idris-lang.org https://www.idris-lang.org
[3] https://github.com/agda/agda https://github.com/agda/agda
[4] https://coq.inria.fr https://coq.inria.fr
[5] https://cicada-lang.org https://cicada-lang.org
[6] https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer
- xvilka 5y agoRegarding Lean I would recommend to check Lean4[1] instead. They rewrote it in Lean itself and now it has much cleaner design[2][3][4]. [1] http://github.com/leanprover/lean4 http://github.com/leanprover/lean4 [2] https://leanprover.github.io/papers/lean4.pdf https://leanprover.github.io/papers/lean4.pdf [3] https://leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf https://leanprover-community.github.io/lt2021/slides/leo-LT2... [4] https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf https://leanprover-community.github.io/lt2021/slides/sebasti...
- iod 5y agoATS Language¹ is another language I would add to this list. First released in 2013, it tries to follow closer to performance and minimalism of C which can make it a good candidate for systems programming². ¹ http://www.ats-lang.org http://www.ats-lang.org ² https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko "A (Not So Gentle) Introduction To Systems Programming In ATS" (2017)
- cloogshicer 5y agoThat ATS video is really good. I think ATS is really fascinating, as it promises full control over the memory layout while also offering strong safety guarantees.
- apatheticonion 5y agoDumb question, is this expressed in TypeScript by the way it offers the ability to write logic inside types using keywords like `infer`, `extends`, `in`, etc? type Foo<T extends Record<any, any>> = { [K in keyof T]: T[K] }
- bmn__ 5y agoNot a dumb question. Answer is no, TS's features are in general not sufficient to express dependent types. It would need to stop making a distinction between types and values, and allow running arbitrary (total) functions in order to define a type, at the least. Experiment with a toy implementation: <https://thelittletyper.com/#pie https://thelittletyper.com/#pie>