5 ms·

I'm nowhere near qualified enough to critique this article in a meaningful manner, but I've been thinking recently that types and compile time functions go hand

I'm nowhere near qualified enough to critique this article in a meaningful manner, but I've been thinking recently that types and compile time functions go hand in hand. Type systems are essentially an attempt to embed a logic that can prove various invariants about the code. What varies across type system to type system is A. what you can express and B. how much you can check. The issue is, most programming language designers decide these two things for you. That's why stuff like reification vs type erasure bites designers; the decision is irreversible. But what if it wasn't? And this seems to be what this article is proposing. That if you can write compile time functions that deal with types as a construct, you can leave decisions like type erasure and reification to the programmer. Granted, that essentially forces programmers to act as language designers. And I doubt most programmers want to learn stuff like type rules or how to prove soundness. However it does have some really cool implications. Like right now, Ruby has this whole debate over adding types. And sure, Ruby could just add normal static typing with some annotations and it'd work. But it kind of doesn't make sense for such a dynamic language to use such a static construct. What'd make more sense (to me) is some sort of metaprogramming on code that allows for checking invariants. Like being able to load a class, then run it through a checker at runtime. I've been reading a book on dependent types (The Little Typer) and the whole idea of types having types with a meta-type of sorts (universes in dependent types, meta classes in Ruby) seems very applicable to Ruby.

reificator 8y ago
Your next step on this journey is to learn a LISP.
- _hardwaregeek 8y ago
  Actually the source for this thought process was going to Racket School and seeing them explain Turnstile and typechecking via syntax-parse and compile time functions :D. It's a fascinating idea but I'm skeptical of the whole "every library is a language" philosophy of Racket scaling. Bugs like infinite compile times are fine when you're writing all the code, but it breaks down when you have libraries.
  - TheDong 8y ago
    As opposed to the current state of the art in more "normal" languages where bugs result in infinite loops / deadlocks at runtime. I've imported many a library which deadlocked, crashed, or infinite looped. In reality it's not that big a deal; it happens and you figure out the bug.
danharaj 8y ago
The main issue is that designing a good type system is a dark art. The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff. Being able to specify your own type language is like having an untyped language governing your term language. There are promising directions though. In 20 years they might even have matured.
- YorkshireSeason 8y ago
  That's the fundamental tradeoff. I'd like to refine this to: the fundamental tradeoff is between expressivity of the typing system and computational complexity of type-inference. Hindley-Milner's polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference. Almost every extension to Hindley-Milner makes full type inference undecidable.
  - danharaj 8y ago
    Type inference is just one part of it. That's taking a term and asking "what type could this have?" Another thing you can do is turn it around and ask "what terms have this type?". That question also gets complicated easily. And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
    - YorkshireSeason 8y ago
      what terms have this type? This is a very interesting question, but one that is rarely asked by compilers or by programmers, or indeed by theoreticians. I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
      - danharaj 8y ago
        Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?". This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156 https://arxiv.org/abs/1607.04156 And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361 https://phabricator.haskell.org/D3361 The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.
naasking 8y ago
> I've been thinking recently that types and compile time functions go hand in hand. Type checking is a stage: http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575 Type systems as macros: http://lambda-the-ultimate.org/node/5426 http://lambda-the-ultimate.org/node/5426
jules 8y ago
Dependently typed languages do use the same evaluation mechanism for the type level and value level. In Java you have List<Int> and that's different than foo(bar), but in dependently typed languages Int is just a value of type Type, and List is a function that takes a Type and returns a Type. The difference is that this evaluation takes place at compile time. For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.

reificator 8y ago

Your next step on this journey is to learn a LISP.

_hardwaregeek 8y ago
Actually the source for this thought process was going to Racket School and seeing them explain Turnstile and typechecking via syntax-parse and compile time functions :D. It's a fascinating idea but I'm skeptical of the whole "every library is a language" philosophy of Racket scaling. Bugs like infinite compile times are fine when you're writing all the code, but it breaks down when you have libraries.
- TheDong 8y ago
  As opposed to the current state of the art in more "normal" languages where bugs result in infinite loops / deadlocks at runtime. I've imported many a library which deadlocked, crashed, or infinite looped. In reality it's not that big a deal; it happens and you figure out the bug.

danharaj 8y ago

The main issue is that designing a good type system is a dark art. The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff. Being able to specify your own type language is like having an untyped language governing your term language. There are promising directions though. In 20 years they might even have matured.

YorkshireSeason 8y ago
That's the fundamental tradeoff. I'd like to refine this to: the fundamental tradeoff is between expressivity of the typing system and computational complexity of type-inference. Hindley-Milner's polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference. Almost every extension to Hindley-Milner makes full type inference undecidable.
- danharaj 8y ago
  Type inference is just one part of it. That's taking a term and asking "what type could this have?" Another thing you can do is turn it around and ask "what terms have this type?". That question also gets complicated easily. And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
  - YorkshireSeason 8y ago
    what terms have this type? This is a very interesting question, but one that is rarely asked by compilers or by programmers, or indeed by theoreticians. I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
    - danharaj 8y ago
      Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?". This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156 https://arxiv.org/abs/1607.04156 And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361 https://phabricator.haskell.org/D3361 The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.

naasking 8y ago

> I've been thinking recently that types and compile time functions go hand in hand. Type checking is a stage: http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575 Type systems as macros: http://lambda-the-ultimate.org/node/5426 http://lambda-the-ultimate.org/node/5426

jules 8y ago

Dependently typed languages do use the same evaluation mechanism for the type level and value level. In Java you have List<Int> and that's different than foo(bar), but in dependently typed languages Int is just a value of type Type, and List is a function that takes a Type and returns a Type. The difference is that this evaluation takes place at compile time. For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.