Re: [Idris] How are the disadvantages of dependent types - general question

[Alex Rozenshteyn]

I'm not an expert on programming with dependent types, but I think I can provide some insight (especially if other people correct my misconceptions).

The biggest disadvantage is novelty. This leads to several other disadvantages:

• For one, programmers have less support when learning to dependently typed programming (DTP). There are fewer examples, the concepts are less ubiquitous in the mainstream, the community is smaller, and there are fewer good/introductory resources (this is a problem that TDD with Idris is chipping away at). This is a social downside, but it's not one to be ignored.
• Another consequence is that languages themselves are less mature. The two languages (that I know of) that are designed primarily for DTP (as opposed to theorem proving or PL research) are Idris and ATS, both of which came about this millennium. Tooling (e.g. IDEs) is okay, but not great (similar claims can be made of languages like Haskell). Compilation has certain problems yet to be solved (e.g. until recently, Idris didn't have a good story for erasing types at runtime, which had big performance costs).
• Some features that we know are coming aren't quite here yet, e.g. term inference (closely related to proof search).
• There are regressions in comparison with other languages (e.g. in Idris, it is not permissible to write a top level term without a type signature).

You might also like to know that DTP is coming to Haskell, slowly but surely.

On Wed, Nov 4, 2015 at 7:52 AM, Carsten Jørgensen <cars...@gmail.com> wrote:

I am reading the Type Driven Development with Idris book by Edwin Brady. I am new to dependent types (but have some experience with F# and Haskell). The book is really cool and dependent types is a fascinating topic. However I cannot stop wondering what the disadvantages of dependent types are. If there were only advantages of dependent types then surely it would already be a feature in e.g. Haskell. 

I do realize that this question is not Idris specific but please help me understand what kind of drawback there are in dependent type languages.

Thanks

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Jonathan Coveney]

I think another non-trivial disadvantage is learning curve. Learning how to properly model solutions in a dependently typed was is pretty difficult, and that dovetails with the novelty, which means there is less material out there to teach people how to do this difficult thing.

[Christopher Allen]

A more serious problem I didn't see mentioned, which doesn't fall under rub-some-community-on-it-and-it-will-go-away is proof churn. Without good proof automation, change a datatype in a decent sized project and your day (week) could be on the wrong foot. This is a lot of why I'm not keen to use DTPLs outside of verified cores/experimentation.

Hopefully David's work creates some options here :)

Chris Allen

Currently working on http://haskellbook.com

[Jan de Muijnck-Hughes]

Erm...I have written a few sizable projects in Idris and my experiences in how long is takes to propagate a change is the same as when I was programming on other languages. I may have not used as much proof automation as others in my programs but changing a data type incurred some cost, but nothing out of the ordinary..

>There are regressions in comparison with other languages (e.g. in Idris, it is not
> permissible to write a top level term without a type signature).

Have to explicitly specify types at the top level, is not a regression. It is an improvement.

Jan

[Alex Rozenshteyn]

>There are regressions in comparison with other languages (e.g. in Idris, it is not
> permissible to write a top level term without a type signature).

Have to explicitly specify types at the top level, is not a regression. It is an improvement.

I emphatically disagree. Any time that the compiler forces the user to write something that it should have been able to figure out on its own, there is a problem. Yes, it is good programming practice to write type signatures on top level terms; but there is a downside to enforcing good practice, namely that your user knows better in this particular case. Paul Chiusano makes a pretty good argument: http://pchiusano.github.io/2015-10-28/top-down.html . My personal issue is that forcing top level type signatures discourages using the language for quick scripts or glue code, since it almost doubles the amount of code I have to write; I've written quick hacks in Haskell, gradually adding type signatures as the code became more complicated, but I would have been very frustrated if I had to annotate e.g. every bytestring constant I defined.

[Jan de Muijnck-Hughes]

I think Paul Chiusano makes a brilliant argument for why we need to be more explicit over the types of our top level functions tbh:

>In better programming environments (like what many dependently-typed languages
> offer), type information we specify gets “pushed down” into our expression, and the
> editor uses it to do more of our work for us or offer more helpful suggestions and
> information.

To be more explicit given the code:

```idris

(++) Nil ys = ys

(++) (x::xs) (ys) = x :: xs ++ ys
```

Can you tell me its type?

Jan

--

[Alex Rozenshteyn]

I could be silly and say something like "(Nil ∈ T a, (a :: T a) ∈ T a) => T a -> T a -> T a", or I could argue against TDNR except via type classes or I could argue that just because Idris _doesn't_ have a type for it doesn't mean that Idris _shouldn't_ have a type for it, but I'll settle for "No, I can't tell you it's type."

A question for you, now. I have three contrived programs; do you believe that the second and third should type error even though the first type checks? Can you convince me?

{-
-- Works
foo : Unit
foo = const () (a + a)
  where a = 0
-}

{-
-- Error, `a` does not have a type signature
a = 0

foo : Unit
foo = const () (a + a)
-}

{-
-- Error, `a` does not have a type signature
foo : Unit
foo = ()
  where a = 0
-}

I'm not arguing that top level terms should never have type signatures; I'm not even arguing that top level terms should always be permitted without type signatures; I'm arguing against the (IMO) unnecessary requirement on top level terms to _always_ have a type signature, even in cases where the language could (reasonably, in principle) infer the type.

[Bryn Keller]

On Wed, Nov 4, 2015 at 10:06 AM, Alex Rozenshteyn <rpglo...@gmail.com> wrote:

I could be silly and say something like "(Nil ∈ T a, (a :: T a) ∈ T a) => T a -> T a -> T a", or I could argue against TDNR except via type classes or I could argue that just because Idris _doesn't_ have a type for it doesn't mean that Idris _shouldn't_ have a type for it, but I'll settle for "No, I can't tell you it's type."

Hi Alex, 

I'm not sure that's so silly, or that you should settle. A human can tell what that code means (perhaps we could argue about whether the length of the sequences should be part of the inferred type as well), why shouldn't Idris (or another language, if need be) be able to? I could be missing something obvious, someone please let me know what it is.

Thanks,

Bryn

[David Christiansen]

> A question for you, now. I have three contrived programs; do you believe
> that the second and third should type error even though the first type
> checks? Can you convince me?

I don't know if I can convince you, but I can at least try to explain
why I think we should require top-level type signatures in all cases,
and how this is different from e.g. Agda, which does not.

In Idris, there is lots of overloading. Lots! For example, the source
code 0 can denote the constructor Z of Nat, the constructor FZ applied
to some implicitly-found Nat in scope, it can be a member of a primitive
type like Int or Integer or Bits8, and it can be an additional
overloading defined in some other module that's been imported.

This means that we would need to wait to determine the type and the
value of your definition "a = 0" until it was used for the first time,
and fail to compile if nothing later constrained it. This would be
difficult, especially if I wanted to be really "kind" to the user and
allow modules that import "a" to be able to determine its type (and
therefore its value) by use. This gets even more difficult with mutual
references.

> I'm not arguing that top level terms should never have type signatures; I'm
> not even arguing that top level terms should always be permitted without
> type signatures; I'm arguing against the (IMO) unnecessary requirement on
> top level terms to _always_ have a type signature, even in cases where the
> language could (reasonably, in principle) infer the type.

I agree, in principle. But there are very, very few such situations in
Idris. And you can get the compiler to write it for you in those cases:

str : ?dunno
str = "What am i?"

If I C-c C-a on ?dunno, I get:

str : String
str = "What am i?"

So I don't think that, in the context of the entire design of the
language, the requirement to annotate top-level definitions is
particularly onerous.

/David

[Alex Rozenshteyn]

Bryn,

It's only silly, really, because I know that's not how Idris works. In a different language, it might be more reasonable. It's also not a principal type (i.e. not the most general type possible; I don't think there is a principal type for that term) because (as you observe) I could define a type (e.g. Vect) which uses the constructors but for which the type given doesn't apply.

--

[Jan de Muijnck-Hughes]

Right;

With hindsight, I realise my last email was more childish than I had originally intended and did not provide a constructive argument for my side. For that I unreservedly apologise. I think everyone can agree that childish arguments are not constructive.

I recognise that you do not believe in the explicit requirement that every top-level term *must* have a type signature, and recognise that we both agree type signatures are important.

Regardless, the point in my original email was that within Dependent types we cannot say for sure what the type of the =(++)= function will be.

We know that it deals with a data type that has constructors =Nil= and =(::)= that do something with two things. However, within the context of Idris prelude and base, let alone user defined types, there will be multiple data types that could be used to construct a type signature. The resulting list of possible types makes this harder to decide without sufficient knowledge: Is it a =Vect= or is it a =List=, or is it some user defined type. If it is a dependent type then there is notions about the values contained within.

For example, in one program in which I had several types that utilises list notation, Idris couldn't tell me which of the five possible data types to chose from.
In another example, it could disambiguate values contained within the types.

My point is that lets be explicit and make disambiguation a easy as possible process.

Jan

[David Christiansen]

Hi Jan

I think you're pointing out a consequence of overloading rather than a
consequence of dependent types per se.

It's still not possible in general to infer most general types - but it
can be possible in special cases. If the only definitions in existence are

data Beer = Pilsner

and I define

tasty = Pilsner

then it would be reasonable for the language to infer

tasty : Beer

But if we had Nat as well, and I wrote

f Z = Pilsner
f (S Z) = Z
f (S (S k)) = f k

then it's probably not reasonable to expect it to infer a type like:

f : (k : Nat) -> if k `mod` 2 == Z then Beer else Nat

This is a consequence of dependent types.

/David

[Alex Rozenshteyn]

David,

I appreciate you taking the time to respond. I understand why Idris makes this a requirement (omitting a type signature is rarely desirable and not worth complicating the compiler for) and I agree with the design choice; that doesn't mean I have to like it.

Jan,

When we can't say what the type of a term is, there are three possibilities:

1. The term represents a program that would "go wrong" at runtime; i.e. it's fundamentally ill-typed
2. The type system in which we are working is insufficiently expressive and we should consider searching for a type system which enables us to type the term
   
3. The type system in which we are working is _sufficiently_ expressive, and the term is pathological; even though it _could_ run, it shouldn't have a type

I tend to prefer the second approach over the third approach. This is a consequence of my perspective on types as extrinsic (i.e. basically entirely erasable, only there to enable early detection of errors), which I think is at odds with dependent types, which AFAICT are usually viewed as intrinsic (i.e. terms have little to no meaning apart from their types).

[Jan de Muijnck-Hughes]

I see your point, and think your example details a reasonable expectation of type inference in a dependently typed language, and why I am in favour of more explicit typing of terms.

Jan

[David Christiansen]

On 04/11/15 20:02, Alex Rozenshteyn wrote:
> I tend to prefer the second approach over the third approach. This is a
> consequence of my perspective on types as extrinsic (i.e. basically
> entirely erasable, only there to enable early detection of errors), which I
> think is at odds with dependent types, which AFAICT are usually viewed as
> intrinsic (i.e. terms have little to no meaning apart from their types).

There are extrinsic dependent type theories out there, as in the
Nuprl/JonPRL/MetaPRL tradition. But yes, we tend to take a types-first
approach in the Idris community.

Both approaches have there merit, and I think in the end, you probably
can achieve systems that are formally translatable to each other, but
the ergonomics will be different.

/D