Re:Dependent Haskell Is the Future (2018)
by lonelappde on Friday August 16, 2019 @07:38AM
(#20714121)
Can a dependently typed list be used in the common case where the length of the list is not known at compile time?
Re:Dependent Haskell Is the Future (2018)
by Legogris on Friday August 16, 2019 @08:08AM
(#20714287)
Yes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this:
app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil ys = ys
app (x :: xs) ys = x :: app xs ys
Re:Dependent Haskell Is the Future (2018)
by andreabedini on Friday August 16, 2019 @08:02AM
(#20714248)
Yes, that’s the whole point of dependent types: types can depend on (runtime) values.
Re:Dependent Haskell Is the Future (2018)
by whateveracct on Friday August 16, 2019 @11:56AM
(#20716444)
Yep - we can even do this today in Haskell without -XDependentTypes :) using things like singletons
You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to.
I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`.
I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself.
There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write.
BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.