Hacker News Reader

Comment by ante_annum | Hacker News Reader

I don't understand what Shen brings to the table that other functional languages don't. Is there a concise imperative of why to learn Shen?

View on HN

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.

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/

It looks like it's a Lisp or Lisp-like, but with some features I haven't seen in other Lisps: pattern matching; currying-by-default; a built-in type system; and so on. IOW it seems like if Lisp and Haskell had a baby.

There's some talk about the motivation here: http://www.shenlanguage.org/motivation.html.

I'll admit that, having studied Haskell before Lisp, I really, really like pattern matching. But I don't think this would be enough for me to pick up Shen; I'd probably go with Clojure if I wanted a Lisp.

I think one of the coolest things I have seen is the way that it has full support for what macro expansion gives you in a "normal lisp" but without the use of quasiquotation - instead it utilizes pattern matching.

Second this. What's Shen's hook? I see a lot of prefix notation for function application...seems Scheme-y to me. I thought things had trended away from that.

Reply on news.ycombinator.com