3 ms·
> The more abstract parts like dependent types are really complicated and even unintuitive to use. I disagree with this: dependent types are way easier than lo
by chriswarbo 5y ago
> The more abstract parts like dependent types are really complicated and even unintuitive to use.
I disagree with this: dependent types are way easier than lots of the convoluted schemes that non-dependent languages have come up with.
As a simple example, dependently-typed languages don't need parametric polymorphism or generics: we can achieve the same thing by passing types as arguments; e.g.
map: (inType: Type) -> (outType: Type) -> (f: inType -> outType) -> (l: List inType) -> List outType
map inType outType f l = match l with
Nil inType -> Nil outType
Cons inType x xs -> Cons outType (f x) (map inType outType f xs)
When I program without dependent types, I regularly find myself getting "stuck" inadvertently; knowing that (a) there's no way to make my current approach work in this language, (b) that it would be trivial to make it work if I could pass around types as values, (c) that I need to throw away what I've done and choose a different solution, and (d) the alternative solution I'll end up with will be less correct and less direct than my original approach (e.g. allowing more invalid states)
- andrewflnr 5y agoIs there work on cleanly subsetting dependently typed languages to ones where well-typed-ness can be automatically proven? That's not generally the case, right? I think those concerns are basically why people come up with less-general typing mechanisms.
- chriswarbo 5y agoThe two main hurdles with dependent types are: - Type-checking is undecidable. I've not found that to be much of a problem, since it can be given a timeout (or hit Ctrl-C). - Soundness requires functions to be total (either terminating or co-terminating). That's generally a good idea anyway, but the approaches for doing this aren't particularly great; e.g. structural recursion is simple to implement and understand, but is very restrictive. Idris makes the pragmatic choice of allowing the totality-checker to be turned off on a per-function basis; which is certainly no worse than using a language with no totality checking. Another approach I've enjoyed using is Mtac in Coq: general recursion is an effect, which gets wrapped in a type (similar to Haskell's IO); there is an unwrapping function (like unsafePerformIO) but it gets executed at compile-time, so non-total functions create an infinite loop at compile time (rather than at runtime).
- dwohnitmok 5y ago> Type-checking is undecidable. This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition). By default in e.g. both Idris and Agda type-checking is decidable.