> As I said, I don't know Idris well, but I assume that the proof language does not have state and other effects, so they need to be coded up as pure functions. I expect there to be an "encoding tax" to be paid for this translation of effects into pure functions.
There is general consensus that the best way to handle effects is a pure base language with an effect system on top. Idris takes a good shot at this, but I doubt it's the last word. Eff and Koka and F* seem particularly promising as well.
> This is not a good analogy, because type-inference can handle parametric polymorphism, whereas general type-dependency on values cannot be dealt in that form.
Why did type inference become the #1 criterion for a type system in this discussion? There are far more important criteria than type inference, such as expressiveness. If your type system is not expressive enough you wouldn't be able to write the program that can't be type inferred at all. Why is that a win?
> Yes, but they are not in your proof language. You can always code up anything.
No sound system can have non terminating functions as proof witnesses. You can reason about potentially non terminating functions just fine in dependently typed languages. Look in particular at NuPRL, which is build around the concept.
> If it's so simple, then we should have systems that do this. We don't have such systems, hence it's probably not that simple.
Doing type inference for non HM-typeable parts of programs is theoretically simple. For the parts of the program that do not have type annotations just type infer them with a HM inference algorithm, if it succeeds great if it fails signal a type error. Just like in ML. The reason that it hasn't been done is likely a combination of reasons (1) not publishable (2) a lot of work (3) type inference just isn't that important especially if you're only doing it for the HM-typeable fragment.
> My experiences in Coq and Agda suggest that that's not the case.
Coq and Agda are not the pinnacle of the possibilities of dependent types. As I said, it's ongoing research. My point is that the style of writing a program and then separately proving lemmas about it is perfectly possible in a dependently typed language.
I would also suggest that your experience may not yet have been that extensive if you didn't know about implicit parameters?
> I don't know what you mean by "implicit parameters". Type inference might be decidable for some weak inexpressive dependently typed systems, but MLTT, CoC, nope?
Implicit parameters let you mark function parameters as implicit and they will be inferred at the call site if the compiler can deduce that they must have one particular value in order for the program to type check. It's like the reverse of type inference: instead of inferring the type of an expression, we infer the expression from the type. It's kind of related to type classes, which let the compiler infer type class dictionaries from types.
Look at the Sage work for full inference for refinement types. I think the same strategy could work for full dependent types. Of course it's not really what you want in practice, since in a dependent type system the most precise type you infer for a function simply restates what the function computes. That is, if you have the function (\x -> x+2) then the type will simply say "a function that returns its argument +2". Inferring the most precise HM type gives reasonable results precisely because HM is weak, so you don't get a type that's "too precise" ;-)
> Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still.
There is general consensus that the best way to handle effects is
a pure base language with an effect system on top.
No, there is absolutely no consensus on this. This approach is only
popular with researchers who pray at the church of lambda.
Essentially all programming languages that are not research prototypes
and that are used in industrial practise don't follow this approach.
There are valid reasons for this. A much better approach in my
opinion is to start with an unrestricted, effectful language and identify fragments with fewer effects via types. The problem is that adding interesting effects effects on top of something super restricted like pure functions leads to a high "encoding tax". That's because pure functions are not very expressive.
Why did type inference become the #1 criterion for a type system
in this discussion?
We have been talking about large-scale software engineering, and
whether Curry-Howard or program logic is a more scalable approach
towards program verification. My claim is that in large-scale software
engineering the single most important criterion is to minimise the
cost of change. Type-inference has 0 cost of change, since it's fully
automatic. I cannot see how a verification tool that I'm forced to use
in prototype phases when there is no stable specification is
cost-effective in large-scale software engineering.
There are far more important criteria than type inference, such
as expressiveness.
Sheer expressiveness is not interesting. You can produce trivial
typing systems where every program is typable. What really matters is
to find "sweetspots" between the following desirable features of
typing systems.
- Expressiveness.
- Strength of properties guaranteed by typing.
- Speed (including decidability) of type-checking or type-inference.
Unfortunately there are hard trade-offs between them.
Doing type inference for non HM-typeable parts of programs is
theoretically simple.
I don't believe it's that simple to do it well, and people do publish
in this area, see for example the Trellys project by Vilhelm Sjöberg.
I think it's an unsolved problem. It may be possible to get a
pragmatically viable system that combines proving and programming in a
unified system, but we are not there yet, and whether the result is
superior to, or on par with simple programming languages and an
associated logic can only be considered when such a language is
available. And note that work like Sjöberg's is about combining pure
functional programming with constructive logic in one system. Even if
some kind of polished Haskell with dependent types can be build,
whether that then generalises to state, concurrency, timing etc in a clean way is
another open question.
I would also suggest that your experience may not yet have been
that extensive if you didn't know about implicit parameters?
Having used Agda, I know about them, I just wasn't sure what you
meant. The term is used in with different meanings in different
contexts. For example they work differently in Scala. And no, it's not
the implicit parameters that make type inference for Agda's MLTT
undecidable.
Look at the Sage work for full inference for refinement types.
Do you mean Cormac Flanagan's Sage? That's not full type inference.
Sage use hybrid type-checking and inserts dynamic checks where type inference fails. This might be
a very good way of doing things in practise, I don't know. Maybe not.
> A much better approach in my opinion is to start with an unrestricted, effectful language and identify fragments with fewer effects via types.
This is precisely what an effect system is, and what the languages that I mentioned do. So it seems that you agree with the the church of lambda on this point?
> We have been talking about large-scale software engineering, and whether Curry-Howard or program logic is a more scalable approach towards program verification. [...] I cannot see how a verification tool that I'm forced to use in prototype phases when there is no stable specification is cost-effective in large-scale software engineering.
I've explained several times that the assumption that you need to do full on verification from the start with a CH style system is incorrect. You can write your prototype without any verification and add lemmas and theorems about it when the spec stabilizes. This is not a fundamental difference between CH style vs program logic style.
> Sheer expressiveness is not interesting. You can produce trivial typing systems where every program is typable.
Well yes, you also need "well typed programs don't go wrong" of course, which dependent type systems do have. I don't think decidability of type checking is desirable, by the way. What you really want is a system that checks statically as much as possible, but can check dynamically that which it can't verify statically. Rather than two possibilities "correct" vs "incorrect" you want three: "definitely correct", "definitely incorrect" and "can't determine statically, so let's check dynamically". In the last case conventional systems just reject the program as incorrect, but I think that is not as helpful.
> Even if some kind of polished Haskell with dependent types can be build, whether that then generalises to state, concurrency, timing etc in a clean way is another open question.
More open than a program logic system that does the same? I don't think the approaches are that different in this regard. With state/concurrency/etc you work with a description of the computation (like in Haskell you work with a description of an IO computation). Those satisfy certain laws which you can use to reason about them. There is of course a huge design space to be explored here, but that design space isn't all that different than the design space of a program logic style system for the same.
> The term is used in with different meanings in different contexts.
I see, yes. They're sometimes called implicit parameters, sometimes implicit arguments, and there's differences in whether only unification is used or also type class / canonical structures / scala style implicit parameters kind of non-canonical inference.
> That's not full type inference. Sage use hybrid type-checking and inserts dynamic checks where type inference fails.
The dynamic checks are for when type checking fails, not type inference. The type inference will always infer the type if the term is typeable. Of course it may sometimes infer a type that the type checker doesn't know statically whether it's valid or not, so you need dynamic checks then. There is no incompleteness defeating magic here, but if the term is typeable then the type inference will infer a type for the term, whether the type checker statically knows that it's valid or not. I did say this was more of a theoretical curiosity.
This is precisely what an effect system is, and what the
languages that I mentioned do. So it seems that you agree with
the the church of lambda on this point?
No, Eff starts with a pure lambda calculus and adds effects on
top.
I've explained several times that the assumption that you need
to do full on verification from the start with a CH style
system is incorrect. You can write your prototype without any
verification and add lemmas and theorems about it when the
spec stabilizes.
As I said, I don't really see that. There is research going on,
like the aforementioned Trelly that seeks to build such systems,
but they are not there yet.
Well yes, you also need "well typed programs don't go wrong"
of course, which dependent type systems do have.
Well typed programs do go wrong! Here is a well-typed Ocaml program:
List.hd [];;
When I run it, an exception is thrown. The point is: what counts
as "not going wrong" is a fairly arbitrary definition. And for
the trivial typing system I can define programs that go wrong as
the empty set.
I don't think decidability of type checking is desirable, by
the way. What you really want is a system that checks
statically as much as possible, but can check dynamically that
which it can't verify statically. Rather than two
possibilities "correct" vs "incorrect" you want
three: "definitely correct", "definitely incorrect" and "can't
determine statically, so let's check dynamically". In the last
case conventional systems just reject the program as
incorrect, but I think that is not as helpful.
I don't think this will be useful, because than every typo will
turn into a dynamic check, and you end up with a dynamically
typed language for all practical purposes. I think
More open than a program logic system that does the same?
Yes, vastly more open. Those problems are essentially solved for
program logics.
I don't think the approaches are that different in this
regard. With state/concurrency/etc you work with a description
of the computation
Yes, you can work by encoding, but then you pay the "encoding
tax" in verification.
The dynamic checks are for when type checking fails, not type
inference. The type inference will always infer the type if the
term is typeable.
That's not how I understand the Sage paper [1], which says: "Our
implementation performs bidirectional type checking (Pierce and Turner
1998), allowing many types to be inferred locally, but does not yet
perform full type inference (a much more technically challenging
problem)."
That paper itself says so in the first sentence?
But the paper also presents a complete inference algorithm for
GADTs. The point is: it depends on exactly what you mean by
GADTs. I don't know what Ocaml does here. I stopped using Ocaml
just before GADTs were added.
There is general consensus that the best way to handle effects is a pure base language with an effect system on top. Idris takes a good shot at this, but I doubt it's the last word. Eff and Koka and F* seem particularly promising as well.
> This is not a good analogy, because type-inference can handle parametric polymorphism, whereas general type-dependency on values cannot be dealt in that form.
Why did type inference become the #1 criterion for a type system in this discussion? There are far more important criteria than type inference, such as expressiveness. If your type system is not expressive enough you wouldn't be able to write the program that can't be type inferred at all. Why is that a win?
> Yes, but they are not in your proof language. You can always code up anything.
No sound system can have non terminating functions as proof witnesses. You can reason about potentially non terminating functions just fine in dependently typed languages. Look in particular at NuPRL, which is build around the concept.
> If it's so simple, then we should have systems that do this. We don't have such systems, hence it's probably not that simple.
Doing type inference for non HM-typeable parts of programs is theoretically simple. For the parts of the program that do not have type annotations just type infer them with a HM inference algorithm, if it succeeds great if it fails signal a type error. Just like in ML. The reason that it hasn't been done is likely a combination of reasons (1) not publishable (2) a lot of work (3) type inference just isn't that important especially if you're only doing it for the HM-typeable fragment.
> My experiences in Coq and Agda suggest that that's not the case.
Coq and Agda are not the pinnacle of the possibilities of dependent types. As I said, it's ongoing research. My point is that the style of writing a program and then separately proving lemmas about it is perfectly possible in a dependently typed language.
I would also suggest that your experience may not yet have been that extensive if you didn't know about implicit parameters?
> I don't know what you mean by "implicit parameters". Type inference might be decidable for some weak inexpressive dependently typed systems, but MLTT, CoC, nope?
Implicit parameters let you mark function parameters as implicit and they will be inferred at the call site if the compiler can deduce that they must have one particular value in order for the program to type check. It's like the reverse of type inference: instead of inferring the type of an expression, we infer the expression from the type. It's kind of related to type classes, which let the compiler infer type class dictionaries from types.
Look at the Sage work for full inference for refinement types. I think the same strategy could work for full dependent types. Of course it's not really what you want in practice, since in a dependent type system the most precise type you infer for a function simply restates what the function computes. That is, if you have the function (\x -> x+2) then the type will simply say "a function that returns its argument +2". Inferring the most precise HM type gives reasonable results precisely because HM is weak, so you don't get a type that's "too precise" ;-)
> Yep, and that preserves type inference, which is the key factor. So it's Hindley-Milner still.
Type inference for GADTs is undecidable.