5 ms·
> 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.
by jules 11y ago
> 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.
Type inference for GADTs is undecidable.
- mafribe 11y agoThere 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. Type inference for GADTs is undecidable. Are you sure? http://research.microsoft.com/pubs/79812/outsidein-icfp09.pdf http://research.microsoft.com/pubs/79812/outsidein-icfp09.pd...