5 ms·
Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.
by turnersr 14y ago
Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.
- pash 14y agoYes. My response was of course to clarify that "ordinary" type systems are Turing equivalent and incorporate classical logic. Dependent types correspond to first-order logic in the Curry-Howard interpretation. I don't know much of anything about Shen, so I can't comment further on it specifically. By the way, limited dependent types can also be implemented in Haskell through type-level programming. The paper that introduced this idea [0] is a good read, and doing some type-level programming is a great way to get to grips with the ins and outs of Haskell's type system. If you're interested in type-level hackery, also be sure to read the HList paper [1]. 0. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2... 1. http://homepages.cwi.nl/~ralf/HList/paper.pdf http://homepages.cwi.nl/~ralf/HList/paper.pdf
- gtani 14y agoThe argument is that agda is relatively straightforward for haskellers and similarly, coq for ocaml devs to adopt. This is a good succinct example of former. Coq has lots of tutorials http://www.cs.uu.nl/education/scripties/pdf.php?SID=INF/SCR-2011-062 http://www.cs.uu.nl/education/scripties/pdf.php?SID=INF/SCR-... There's also typed racket, which i don't know anything, it's been mentioned to me as "theorems for free" http://docs.racket-lang.org/ts-guide/ http://docs.racket-lang.org/ts-guide/