Why dependent types matter

View 1 excerpt, cites methods. Dependently typed programming in Agda. View 3 excerpts. Dependent type systems allow for a rich set of program properties to be expressed and mechanically verified via type checking. However, despite their significant expressive power, dependent types … Expand.

View 2 excerpts, cites background. Constrained types for object-oriented languages. View 1 excerpt. Introducing Type Properties. Dynamic optimization for functional reactive programming using generalized algebraic data types. Dependent types in practical programming. We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML C language … Expand. Dependently typed functional programs and their proofs.

Practical implementation of a dependently typed functional programming language. Typing dynamic typing. Accessed A dependent type is a type that depends, not just on other types, but on terms.

This means you can have values — plain old data — in your types. A common example is that of length-indexed lists :. You likely caught on that that code is Swift-ish but not actually Swift. We no longer need separate, parallel languages for working with types like Int or String vs working with terms in those types like 3 or "perish the thought". Dependent types make it possible to be very specific about the terms in a type.

This means that dependent types give us pay-as-you-go provable correctness. Imagine the horror This isn't to say that they should abandon Epigram. I was merely talking about the best way to evangelize dependent type systems. But this discussion does bring us to a more general question, i. Notice that not everyone follows this approach. This is just one style of doing PL research. By Ehud Lamm at Fri, login or register to post comments features Ehud was asking whether it makes sense to design a new language for every feature we want to explore.

Obviously not. On the other hand I see people adding feature after feature to Haskell's type system, and can't help noticing that most of the new and many of the old features would be subsumed by having a access to full dependent types.

Hence, I would say that while a new language for every feature is certainly not a good idea, at some point it pays off to be more radical and move to a new language instead of trying to fix the old one. My original point was that I think many more would come to appreciate the ideas you are advocating in this paper if at least some of the example would have been given using more familiar syntax. By Ehud Lamm at Sat, login or register to post comments Need both You need a language where the expression of the ideas is natural and easy.

But you also need to show how these things can be expressed in the more common languages warts and all. I disagree, in this case. This paper gave me a bunch of "aha" moments about dependent typing, and inspired me to start playing around with Epigram. I doubt I would have been so excited if it had been loaded down with encodings into GADTs and caveats about current FP implementations.

Finally we see an example of using dependent types to enforce something more complicated than a datatype shape constraint. The examples I'd seen up until now were so small that I didn't see how dependent types or GADTs could help me prove anything interesting about my programs. I've been reading both the Omega papers and the Epigram papers as they appear on LtU; it's wonderful to have these exemplars of dependent typing developing in parallel.

On the other hand, Epigram knocks my socks off, even though it's eminently less practical. It's the first formalism I've seen in which both programs and proofs felt natural.

A bit more friendliness in the editor, and I could see myself getting addicted No Ehud, you are not the only one Haskell is evolving towards dependent types e. GADTs and that's a good thing. Epigram is a more radical departure, I believe we discuss the tension in the conclusions of the paper. I'm a professional programmer and I'd like to understand this paper, but I don' t have a degree in CS, so I'm a bit lost when it comes to formalisms. Check out this thread for references.

The link in Koray Can's reply is good. In the meantime, the statement in YDTM is based on the Curry-Howard isomorphism between logic and lambda calculus, the basis of functional programming. Types correspond to propositions, and the logical proposition in the subject line is certainly false.

One thing I didn't see though, is any kind of tutorial on the symbols and notations used in this paper. I'm simply not familiar with their meaning. I didn't know that upside down A means "for all" until I inferred it from Jim's reply. Is there a resource available that will help me decode the symbols and formulas?

Mathworld and Wikipedia can sometimes be useful for this sort of thing, although I imagine finding something if you only know the symbol could be difficult. Here's another page about quantifiers. By Anton van Straaten at Thu, login or register to post comments I've tried to teach people autodidactism I've tried to teach people autodidactism, but I've realized they have to learn it for themselves.

Symbol definition is a common problem for me too. I often jump into a new subject area and realize that no amount of tutorials will help until I know the symbols. If there existed a symbol lookup tool or website that included contextual usage, I could teach myself new things in less time.

For example, I don't think that the concepts in the Bananas, Lenses, and Barbed Wire paper are difficult, the hardest part for me was discovering what the symbols meant. Wikipedia is improving the lives of autodidacts like me! Maybe this would be a useful point for the proposed LtUpedia wiki.

No kidding! Via CH Y id the non-terminating computation is the proof. I don't know a good introduction to constructive mathematics for computer scientists. I hope that my lecture notes for my Math for Computer Science course will some day evolve to such a thing but for the moment In any case maybe the best way to learn the stuff is by playing around with it: Conor has written an excellent tutorial for Epigram and the system is available for free from our webpage under reconstruction and runs on Windows, Linux and MacOs.

A new release is under development any volunteers to help with the GUI? I spent a couple of days assessing efforts and ways to build an editor for Epigram in Eclipse. I have more experience in graphical editors, but Epigram calls more for a rich text. Also, at that moment about a year ago my understanding of dependent types was much worse than today which is still very basic A big problem is that editor is actually interacting heavily with elaborator, for which I don't think there is Java API one could try to use it via stdio.

My final suspiction is that to make any sense from engineering point of view the official IDE should share the implementation language with other subsystems, so either it should be Haskell based or the existing Epigram rewritten in Java oh, never! Uh, there is always an option of self-hosting, but for that Epigram must probably be embedded as rule language into some rewriting system only half-joking here. By Andris Birkmanis at Sun, login or register to post comments Epigram editor interface One of the alternatives we consider is to have a language independent interface between elaborator and IDE.

This doesn't look to difficult. In this case we could plug in different IDE variants. You didn't say what the results of your assessment wrt. Eclispe were. It is unlikely that we would want to rewrite Epigram in Java.

I'd rather hope that we implement it in Epigram one day One of the alternatives we consider is to have a language independent interface between elaborator and IDE. I am not sure they are worth much, as YMMV greatly, as you know. I would say, it would take from 2 weeks for base functionality to 2 months for 1st release - but working at optimal schedule and assuming interface to elaborator is ready.

One of my biggest concerns is - why? There are two reasons I see for doing it in Eclipse - popularizing Epigram as using Eclipse is pretty popular and acquiring a good development team as hacking Eclipse is pretty popular. OTOH, I am not sure the same cannot be said about Emacs yes, it's not in vogue in certain circles Or the editor?

For latter you probably need to not only ensure Turing completeness, but more importantly - interactiveness, that's why I was kidding about rewriting systems. Oh the magical Turing completeness again.