5 ms·

> I don't know if there exists any type that can't be expressed in Scala. Scala has a very rich type system, but let us not get ahead of ourselves--Scala, bein

> I don't know if there exists any type that can't be expressed in Scala. Scala has a very rich type system, but let us not get ahead of ourselves--Scala, being non-dependently typed, cannot type many useful programs. For an example of a useful dependent type, consider giving division the type Number -> {x : Number | x != 0} -> Number. Giving division the type Number -> Number -> Number is similar to how older Javas would type List<String> as List and require all get operations to cast from Object--in both cases, the type system is unable to guarantee that your program won't crash. If you want a glimpse of the state of the art of programming with dependent types, try Agda[0]. [0]: http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php

TylerE 13y ago
How does that actually work? Does that "type" basically compile down to an added n != 0 check at runtime, or is there more sophisticated dataflow analysis/theorem proving going on?
- tel 13y ago
  Usually it enforces statically that you cannot create an Integer that violates its preconditions. If you even do so dynamically it'll make sure there's a dynamic check before the dynamic value can substantiate the more specific type.
  - jroesch 13y ago
    It is done statically. Types are a compile time construct, languages like Agda and Coq have no type information at runtime. This means if one can't statically prove that their types are correct the code won't compile. For example if my function returns a Vector[A, N] (a vector of A's with size N), and I try to pass it's return value to a function that expects a of type Vector[A, 2] my code will not compile. This is because there is no way one can prove forall A N. Vector[A, N] satisfies Vector[A, 2].
    - tel 13y ago
      Not all things are statically checkable. If you want to take in some runtime data and treat it as a Vector[A, 3] then you'll need to include a dynamically failing check like (List -> Maybe (Vector n a)).
      - ajanuary 13y ago
        I don't know Agda or Coq but I assume all it would take is to test the size and throw a runtime error for it to statically assert that it is the correct size after the test. Now the compiler is helping you write the runtime preconditions checks and handling that you should be writing anyway.
        tel 13y ago
        Yeah, that's exactly how dynamic data can enter a statically typed regime of code. Dependent types make it so that it's impossible to bring dynamic data into type-controlled parts of your code without first performing and passing those tests. Which seems weak since smart developers should do that anyway, but (a) there's still some divide between "should" and "it's impossible" and (b) this is just the tip of the iceberg about what dependent types offer anyway.
- Sae5waip 13y ago
  The latter. Check out https://en.wikipedia.org/wiki/Agda_(programming_language) https://en.wikipedia.org/wiki/Agda_(programming_language)
- chrismonsanto 13y ago
  It depends. In the most general case, you have to prove that the program you have given has the type you have asserted. This is similar to proving a mathematical theorem. Generally, the computer will assist you in this endeavor--for example, if you want to prove that A implies B, and A and B are linear inequalities, this can be solved automatically.
  - Locke1689 13y ago
    Generally, the computer will assist you in this endeavor Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.
    - chrismonsanto 13y ago
      I have faith that this will get better. We need standard libraries of proofs just as much as we need standard libraries of code. I know Coq has made progress on this, but it's still early days. I do agree with you that there are times when 'full' type checking is inappropriate. Typing is a spectrum, and it's a bit of an art to decide how detailed of guarantees to give for your API.
    - bootily 13y ago
      That is hilarious. And I also hope your joking.
      - chrismonsanto 13y ago
        That user is not joking, but note that you generally prove that string concatenation is associative once, not every time.
thinkpad20 13y ago
Agda and Idris are both very interesting to me, especially the latter since it was designed with systems programming (read: real-world applications) at its core. They both seem kind of like beefed-up Haskell. However, I wonder how much actual utility they can provide, seeing as (1) dependent typing is generally acknowledged to be rather difficult (and that's a statement coming from those who generally tend to already be good at a language like Haskell), and then also (2) the fact that a great deal of real-world applications, such as FFI, accepting data over a wire, dealing with exceptions and faulty input, etc, mean that no matter how bullet-proof the code you write is, you'll still have to account for all of the ugliness which the world can throw at you, which means unit testing, exception handling and other things which seem to undermine - to a degree - the strengths of strong typing in the first place. Or am I exaggerating things? I've written a lot in Haskell and enjoy it a great deal, but at work I use Python and JavaScript, and honestly, although there are some things that would be streamlined away by a strong typing system, particularly in the development cycle, there are still a ton of ugly, mundane real-world things that would still need to be dealt with in much the same way if they were written in Haskell. I would still love to have the opportunity to write in Haskell (or Agda or Idris, etc) at work, but I'm not sure how much trouble it would save me from at the end of the day. Would it? And would the additional mental hurdles of dependent typing add real tangible benefits on top of this?
pkinsky 13y ago
You can use pattern matching with custom extractors to define partial functions only accepting positive numbers. object Positive { def unapply(x: Int): Option[Int] = if (x>0) Some(x) else None } val onlyPositive: PartialFunction[Int, String] = { case Positive(x) => s"check out this positive number: $x" } This would throw a MatchError for non-positive Ints, but you can also handle the failure case like so: def onlyPositive(n: Int) = n match { case Positive(x) => s"check out this positive number: $x" case _ => s"not a positive number: $n" } This is a quick example, but in practice the lack of dependent types is not a huge handicap.

TylerE 13y ago

How does that actually work? Does that "type" basically compile down to an added n != 0 check at runtime, or is there more sophisticated dataflow analysis/theorem proving going on?

tel 13y ago
Usually it enforces statically that you cannot create an Integer that violates its preconditions. If you even do so dynamically it'll make sure there's a dynamic check before the dynamic value can substantiate the more specific type.
- jroesch 13y ago
  It is done statically. Types are a compile time construct, languages like Agda and Coq have no type information at runtime. This means if one can't statically prove that their types are correct the code won't compile. For example if my function returns a Vector[A, N] (a vector of A's with size N), and I try to pass it's return value to a function that expects a of type Vector[A, 2] my code will not compile. This is because there is no way one can prove forall A N. Vector[A, N] satisfies Vector[A, 2].
  - tel 13y ago
    Not all things are statically checkable. If you want to take in some runtime data and treat it as a Vector[A, 3] then you'll need to include a dynamically failing check like (List -> Maybe (Vector n a)).
    - ajanuary 13y ago
      I don't know Agda or Coq but I assume all it would take is to test the size and throw a runtime error for it to statically assert that it is the correct size after the test. Now the compiler is helping you write the runtime preconditions checks and handling that you should be writing anyway.
      - tel 13y ago
        Yeah, that's exactly how dynamic data can enter a statically typed regime of code. Dependent types make it so that it's impossible to bring dynamic data into type-controlled parts of your code without first performing and passing those tests. Which seems weak since smart developers should do that anyway, but (a) there's still some divide between "should" and "it's impossible" and (b) this is just the tip of the iceberg about what dependent types offer anyway.
Sae5waip 13y ago
The latter. Check out https://en.wikipedia.org/wiki/Agda_(programming_language) https://en.wikipedia.org/wiki/Agda_(programming_language)
chrismonsanto 13y ago
It depends. In the most general case, you have to prove that the program you have given has the type you have asserted. This is similar to proving a mathematical theorem. Generally, the computer will assist you in this endeavor--for example, if you want to prove that A implies B, and A and B are linear inequalities, this can be solved automatically.
- Locke1689 13y ago
  Generally, the computer will assist you in this endeavor Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.
  - chrismonsanto 13y ago
    I have faith that this will get better. We need standard libraries of proofs just as much as we need standard libraries of code. I know Coq has made progress on this, but it's still early days. I do agree with you that there are times when 'full' type checking is inappropriate. Typing is a spectrum, and it's a bit of an art to decide how detailed of guarantees to give for your API.
  - bootily 13y ago
    That is hilarious. And I also hope your joking.
    - chrismonsanto 13y ago
      That user is not joking, but note that you generally prove that string concatenation is associative once, not every time.

thinkpad20 13y ago

Agda and Idris are both very interesting to me, especially the latter since it was designed with systems programming (read: real-world applications) at its core. They both seem kind of like beefed-up Haskell. However, I wonder how much actual utility they can provide, seeing as (1) dependent typing is generally acknowledged to be rather difficult (and that's a statement coming from those who generally tend to already be good at a language like Haskell), and then also (2) the fact that a great deal of real-world applications, such as FFI, accepting data over a wire, dealing with exceptions and faulty input, etc, mean that no matter how bullet-proof the code you write is, you'll still have to account for all of the ugliness which the world can throw at you, which means unit testing, exception handling and other things which seem to undermine - to a degree - the strengths of strong typing in the first place. Or am I exaggerating things? I've written a lot in Haskell and enjoy it a great deal, but at work I use Python and JavaScript, and honestly, although there are some things that would be streamlined away by a strong typing system, particularly in the development cycle, there are still a ton of ugly, mundane real-world things that would still need to be dealt with in much the same way if they were written in Haskell. I would still love to have the opportunity to write in Haskell (or Agda or Idris, etc) at work, but I'm not sure how much trouble it would save me from at the end of the day. Would it? And would the additional mental hurdles of dependent typing add real tangible benefits on top of this?

pkinsky 13y ago

You can use pattern matching with custom extractors to define partial functions only accepting positive numbers. object Positive { def unapply(x: Int): Option[Int] = if (x>0) Some(x) else None } val onlyPositive: PartialFunction[Int, String] = { case Positive(x) => s"check out this positive number: $x" } This would throw a MatchError for non-positive Ints, but you can also handle the failure case like so: def onlyPositive(n: Int) = n match { case Positive(x) => s"check out this positive number: $x" case _ => s"not a positive number: $n" } This is a quick example, but in practice the lack of dependent types is not a huge handicap.