4 ms·

> So, let's make an odd_int_less_than_20587 type and a billion of other types? I see your point, but I think that (while not always), it can still be pretty he

by JD557 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? I see your point, but I think that (while not always), it can still be pretty helpful to add your custom types to make invalid states unrepresentable. This can sound ridiculous on something like C, but if your language has refined types, it's not that bad. For example, this doesn't look awful to me: ``` type WeirdId = Int Refined (Odd And Less[20587]) val myId: WeirdId = 5 // OK val myInt: Int = myId // Can be used as an Int val myRuntimeId: Either[String, WeirdId] = refineV[Odd And Less[20587]](myId + 2) // Runtime Check val myInvalidId: WeirdId = 6 // Compilation Error ``` https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA

jstimpfle 5y ago
I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-level and code level, and I'm completely fine with sprinkling a few runtime assertions in most cases. Normal code syntax is much more suited to expressing invariants. Obviously I'm not into statically proving the correctness of my programs, so if that's your cup of tea things are probably looking different (and I'm sorry for you).
- atq2119 5y ago
  I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.
  - captainmuon 5y ago
    Exactly. It pains me when someone comes up with a new language with dependent types, but then to encode a simple constraint they first define integers via peano axioms using some kind of template metaprogramming. (The example I'm remembering was Coq or a Haskell dialect or something.) There was a dialect of C#, Sing# or Spec#, that allowed you to specifying pre and post conditions in the same expression language as the main language, and they were checked at compile time. This is what comes closest I think.

by JD557 5y ago

jstimpfle 5y ago

I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-level and code level, and I'm completely fine with sprinkling a few runtime assertions in most cases. Normal code syntax is much more suited to expressing invariants. Obviously I'm not into statically proving the correctness of my programs, so if that's your cup of tea things are probably looking different (and I'm sorry for you).

atq2119 5y ago
I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.
- captainmuon 5y ago
  Exactly. It pains me when someone comes up with a new language with dependent types, but then to encode a simple constraint they first define integers via peano axioms using some kind of template metaprogramming. (The example I'm remembering was Coq or a Haskell dialect or something.) There was a dialect of C#, Sing# or Spec#, that allowed you to specifying pre and post conditions in the same expression language as the main language, and they were checked at compile time. This is what comes closest I think.