www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Dependent types & ATS language

I am learning something about the Dependent Types, it's a type of type system.
Some of you may be interested, so here are few notes.

There's a Wikipedia page about Dependent types, but it doesn't explain enough
for me, so no URL here. 

As it often happens, those someone has put part of those computer science ideas
inside a programming language, this is named ATS. If programmed well it is
about as fast as C, it allows some theorem proving, it may be used to write
Linux device drivers, and it has Dependent types (and linear types):
http://en.wikipedia.org/wiki/ATS_%28programming_language%29

I have started to understand dependent types and what's good in them after
reading this page, that while surely showing not much about ATS, shows some
ideas that I didn't know:
http://www.bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html

There are other languages for theorem proving like Coq, but they look even
harder to use than ATS.

Using ATS its author was able to create a (not efficient, list-based) QuickSort
that guarantees that it always returns a list that is a sorted permutation of
its input, this is not an easy feat at all:
http://www.ats-lang.org/EXAMPLE/MISC/listquicksort_dats.html

But what has sold me on the dependent types is this, it implements red-black
trees, this ATS program implements the insertion and balancing, plus
correctness proof, so probably this is correct code:
http://www.bluishcoder.co.nz/ats/dt8.dats

If you have tried to implement red-black trees in C you know that you produce a
four times longer program that often at the first implementation contains some
hard to find bugs.

ATS is not a general purpose language, it's for low-level code that needs to be
a bit safer.

Bye,
bearophile
Oct 15 2010