What is 'dependent typing'?
Author
I first heard about dependent typing in reference to Epigram Language from this thread. I tried to read about it but unfortunately all information I could find was either very abstract or extremely theoretical. Can someone explain what it is in plain english or perhaps provide a reference to relevant resources?
In C++ (that may not be what the AP was referring to)
T::iterator and Base<V> are dependent types - the type you're referring to depends on what T and V are in the template that are using those types.
template<class T> typename T::iterator begin(T& container){ return container.begin();}template<class T> struct Base {};template<class V> struct Derived : Base<V> {}T::iterator and Base<V> are dependent types - the type you're referring to depends on what T and V are in the template that are using those types.
The tutorial has some easy and understandable examples (if you know haskell or a similar language).
In plain words: Dependant typing allows type to depend on value, especially the type of functions may depend on the value of the arguments. An empty list can have another type than one which contains something. Type information on lists can contain the number of elements.
C++ templates are similar. I am not sure how they differ in detail. Strictly speaking templates aren't types.
In plain words: Dependant typing allows type to depend on value, especially the type of functions may depend on the value of the arguments. An empty list can have another type than one which contains something. Type information on lists can contain the number of elements.
C++ templates are similar. I am not sure how they differ in detail. Strictly speaking templates aren't types.
Author
Quote:Original post by Trap
The tutorial has some easy and understandable examples (if you know haskell or a similar language).
Unfortunately, I don't [sad] I have a rather limited knowledge of lisp, though.
Quote:Original post by Trap
In plain words: Dependant typing allows type to depend on value, especially the type of functions may depend on the value of the arguments. An empty list can have another type than one which contains something. Type information on lists can contain the number of elements.
Ahh, I see. So what's the perceived usefulness of this and what shortcomings is it trying to solve?
BigList : lists where size > 3 elementsSmallList : lists where size is <= 3 elementsl = [1, 2];At this point l is of type SmallList. What does this buy me aside from not having to manually introduce if statements in my functions that accept lists to check for their size (not that this isn't a significant win)?
Lisp isn't similar at all in this aspect, Haskell is to types and typing what Lisp is to parentheses ;)
There is 1 special kind of dependant type in some languages: fixed size arrays
Dependant typing allows a lot of IDE-assistance while writing functions, the IDE can guide your way to writing a total function. You can't miss special cases, because you only pick a strategy and the IDE automatically list all cases.
There is 1 special kind of dependant type in some languages: fixed size arrays
Dependant typing allows a lot of IDE-assistance while writing functions, the IDE can guide your way to writing a total function. You can't miss special cases, because you only pick a strategy and the IDE automatically list all cases.
Author
Quote:Original post by Trap
Dependant typing allows a lot of IDE-assistance while writing functions, the IDE can guide your way to writing a total function.
Ahh, I see. Another interesting thing would be proving correctness/ensuring safety, wouldn't it? For instance, if you iterate over an array with an int [0, 10] type, you don't need bounds checking because your tools could prove at compile time whether you're overrunning the bounds. I'm not sure how this would work in practice though... Iterating over an array is a fairly simple example but what about IDE assistance? Can you give an example of that? Do you know of any tools that implement such system at least partially?
There is a packet that works with xemacs at the epigram site, haven't you tried it? It works somewhat, but i couldn't even get the examples to work. Perhaps because i haven't read the docs carefully.
Author
Quote:Original post by Trap
There is a packet that works with xemacs at the epigram site, haven't you tried it? It works somewhat, but i couldn't even get the examples to work. Perhaps because i haven't read the docs carefully.
Well, it specifically says that it's very very preliminary. I was hoping there are better tools out there to test out the idea. Perhaps I should take some time to learn Haskell as it looks fairly interesting (though whenever I see pattern matching in a language, I run [smile]) It looks like Haskell is designed to do some compile time proofs of correctness as well, right? Is it actually useful in real life? I haven't heard much about it outside of academic circles.
The example package is still worth trying, it is an interesting experience to interact with it.
For a language that only supports church numerals it has a great ide ;)
Im not fluent in writing haskell but i can read it. I don't think there is any prover in it, only type inference and strong static typing. Haskell is a nice language to program or prototype algorithms in, but doing any kind of imperative stuff like IO gets ugly very quickly. Maybe not if you are really fluent in it, but i am not, i'm happy to have the compiler accept my code.
For a language that only supports church numerals it has a great ide ;)
Im not fluent in writing haskell but i can read it. I don't think there is any prover in it, only type inference and strong static typing. Haskell is a nice language to program or prototype algorithms in, but doing any kind of imperative stuff like IO gets ugly very quickly. Maybe not if you are really fluent in it, but i am not, i'm happy to have the compiler accept my code.
This topic is closed to new replies.
Advertisement
Popular Topics
Advertisement
