Hacker News Reader

Comment by lmkg | Hacker News Reader

It seems like Shen is a successor to Qi, which if I remember right, had a type system that incorporated full-blown classical logic. If Shen follows in this tradition, then its type system would be significantly more expressive than standard functional type systems. It would allow not only arbitrary predicates on input and output, but also relationships between them. Needless to say, such a type system is Turing-complete, and therefore not guaranteed to terminate.

Systems like this are usually used as theorem-proving systems, not actual production languages. I think Qi was intended to be a practical language that allowed arbitrary proofs about the properties of its programs.

I have not been able to find any reference to this in a quick perusal of Shen's documentation.

View on HN

Standard type systems are Turing equivalent. This includes the type systems of functional languages like ML and Haskell. In fact, there's a neat correspondence [0] between algebraic data types and propositional logic (examples in Haskell):

  union types (data T = mkTA A | mkTB B) <-> logical disjunction (A ∨ B)

        product types (data T = mkT A B) <-> logical conjunction (A ∧ B)

        function types (type T = A -> B) <-> logical implication (A → B)

                      the unit type (()) <-> true (⊤)

                              bottom (⊥) <-> false (⊥)

(And, if you were wondering, that's where the symbol for "bottom" comes from!)

Inference on richer type systems, e.g., systems that support dependent types (types built up from expressions about the values they represent) is in general undecidable, which is why some dependently typed languages (e.g., Coq) have type systems that are not Turing equivalent—the language designers have consciously pared down parts of the type system in order to guarantee that type-checking terminates.

0. This is the Curry-Howard correspondence: http://en.wikipedia.org/wiki/Curry–Howard_correspondence#Cor...

Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.

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

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/

Reply on news.ycombinator.com