Which dependently typed programming languages could be used for real world application development? I will mostly be writing toy applications at first, after that maybe web development or a simple DBMS.

These are some points, that I think are important:

  • documentation
  • example programs
  • a good/big standard library
  • an easy to use foreign function interface
  • a community of people using the language for real world tasks
  • tool support

I am aware that there is currently no language that meets all these requirements. I'd like to know which one comes closest.


Unfortunately, you are asking for something that just doesn't exist yet. Things such as big libraries, etc general only come with maturity + large community bases, of which they have no reached.

You can find a list of them on Wikipedia, which will at least let you filter out those that are not actively developed.

What are you reasons for wanting to use a dependently-typed language for web development, etc?

| improve this answer | |
  • 1
    I've been playing around with ATS a bit. I'm mostly just curious whether it can be done and whether it would actually have advantages over languages without dependent types. Is there a language with a cgi interface or any other kind of integration with a web server? I know the wikipedia list... – Kim Jan 9 '11 at 6:37
  • If you can make it an executable you can surely make it work with CGI. Have I seen any? No. Can I find any? No. I'm not sure what advantages it would have over the current prevailing languages though... – Dan McGrath Jan 9 '11 at 11:00

Probably Agda is the most alive of these, but it's hardly 'commercial grade' software yet, it's more 'bleeding edge'.

| improve this answer | |

Not the answer you're looking for? Browse other questions tagged or ask your own question.