3 ms·

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?

deleted 14y ago
[deleted]
cantankerous 14y ago
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.
lmkg 14y ago
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.
- pash 14y ago
  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#Correspondence_between_classical_logic_and_control_operators http://en.wikipedia.org/wiki/Curry–Howard_correspondence#Cor...
  - turnersr 14y ago
    Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.
    - pash 14y ago
      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.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 ago
        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-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/
wonderzombie 14y ago
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 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.
shaunxcode 14y ago
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.

deleted 14y ago

[deleted]

cantankerous 14y ago

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.

lmkg 14y ago

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.

pash 14y ago
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#Correspondence_between_classical_logic_and_control_operators http://en.wikipedia.org/wiki/Curry–Howard_correspondence#Cor...
- turnersr 14y ago
  Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.
  - pash 14y ago
    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.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 ago
      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-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/

wonderzombie 14y ago

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 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.

shaunxcode 14y ago

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.