4 ms·

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 s

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.

lisper 13y ago
> ensure_conforms_to(int) Why int? What about adding floats? complex numbers? rationals? quaternions? matrices? dimensional quantities? etc. etc. etc.
- breckinloggins 13y ago
  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.
  - lisper 13y ago
    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.
    - breckinloggins 13y ago
      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/ http://www.idris-lang.org/
      - tel 13y ago
        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.

lisper 13y ago

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

breckinloggins 13y ago
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.
- lisper 13y ago
  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.
  - breckinloggins 13y ago
    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/ http://www.idris-lang.org/
    - tel 13y ago
      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.