News for hackers. Stuff that matters.

A comment on Learn Shen. Parent comment

Re:Learn Shen by pash on Thursday November 01, 2012 @11:46PM (#4731144)
Yes. 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.2...

1. http://homepages.cwi.nl/~ralf/HList/paper.pdf

[ Parent | on HN ]
Re:Learn Shen by gtani on Friday November 02, 2012 @01:54AM (#4731422)
The 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-...

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/

[ Parent | on HN ]