Hacker News Reader

Comment by keppy | Hacker News Reader

Shen/Qi was the first Fluchtpunktish lisp I ever spent time with, and I had not used any typing system outside of Typed Racket and some other hand-made implementations. I remember being amazed that the Shen type system isn't more widely used across more domains. Once you start using it, you feel like the type problem is 'solved' in Shen. The author is right on about this language offering something special--Shen is one of those addictive hammers that you will want to hit all the nails with. More importantly it's a type system that can be used in conjunction with existing systems or even implemented in a different language. A good test for how powerful a new means of abstraction actually is, is to try using it outside of its original implementation.

View on HN

I agree. In my opinion the whole notion of a baked-in "type system" is silly. Type systems themselves aren't silly, but including one in the language proper seems to be stopping at the wrong abstraction.

Let's say we see:

    int add_two(int a, int b)

We're so used to seeing those "ints" as types, but why? There's a better abstraction here, mainly one of:

    ensure_conforms_to(int) add_two(ensure_conforms_to(int, a), ensure_conforms_to(int, b))

I'm not arguing for that horrific syntax, I'm saying that type systems are just another part of your program running at a separate time. There's a LOT more you can do with that concept than just enforcing and deducing the tags and acceptable conversions that go with values. Contracts, powerful dispatch mechanisms, ad-hoc optimization strategies, complex lambda cube stuff like dependent types... all of these things can be served with the right abstraction.

And there is no reason that your editors, documentation browsers, code completion engines, syntax highlighters, debuggers, and every other part of your environment can't use it!

Shen seems to get that.

> ensure_conforms_to(int)

Why int? What about adding floats? complex numbers? rationals? quaternions? matrices? dimensional quantities? etc. etc. etc.

That was, of course, just an example. I'm also assuming that any "real" type system implemented this way would do this with something like typeclasses or higher kinds or something else.

The larger point is that baked-in type system see the word "int" as a type, but what that's hiding is the higher abstraction: that what we're really doing is specifying a function which should be run when determining the validity of the program.

But that was exactly my point: what IS this "higher abstraction" to which you allude? What are you actually advocating here? Typeclasses? Sequent calculus? Something else? Details matter.

I'm advocating something that typeclasses, sequent calculus, contracts, etc. could be built on. Sure, the language may have some standard libraries that would do much the same things that these do in other languages, but those libraries could be improved, removed, or replaced by the programmer.

What exactly is the point of a type system? I think there are really two big ones: program verification and metadata tagging. To simplify, the former is why Haskellers love types, and the latter seems to be the main reason that F#'s type providers exist (and why C# programmers love creating lots of little types rather than using typeless object literals a la Ruby).

Intellisense is an incredibly seductive thing, and many programmers in the enterprise world would argue that any language that can't show you that little "box" after you press Ctrl+Space is dead on arrival.

But both of those things are a subset of the things you COULD do if the phases of compilation were in your control. Maybe you want a function that says "throw an error at compile time if someone uses this deprecated parameter on this API call", or maybe you'd like to have a function where if you call it with a hard-coded URL, the program fails at compile time if the URL can't be reached.

These are obviously a bit silly, but the point is that, to many of us, WHENEVER a compiler is doing something with our AST, that should be fully exposed and not a black box. Another example: why is Idris[1] its own language? Why isn't it just a Haskell library? Granted that also gets into programmable syntax and editor support thereof, but that's part of my larger point as well.

[1] http://www.idris-lang.org/

One reason why Idris is its own language is that you can't just lie dependent types atop a language---that's the whole point, the types interact with the values and the values the types. This blurs the boundary between compiler phases.

Sometimes you get type erasure, but for really interesting programs to arise (the kind that I'm sure Idris is aiming at, though I don't know for certain) you really want to operate in that blurry divide.

Anyone with experience with both Shen/Qi and an HM type system (OCaml, Scala, Haskell family) able to comment? I'd love to learn a bit more about what Shen/Qi do.

Scala does not use an HM type system. This is actually its most significant fault, and much code is written to sweep the matter under the rug.

I thought it was still "locally HM-like", but I don't really have a clue what type systems including class hierarchies look like.

Its most significant fault and also its greatest virtue: there's no way to integrate Java's type system into a proper HM type system. As Scala's (mostly) seamless, bidirectional Java integration is its prime selling point (otherwise, why not just use Haskell?), this complaint mostly misses the point.

Reply on news.ycombinator.com