# Unity What is 'dependent typing'?

This topic is 4906 days old which is more than the 365 day threshold we allow for new replies. Please post a new topic.

## Recommended Posts

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?

##### Share on other sites
In C++ (that may not be what the AP was referring to)

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.

##### Share on other sites
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.

##### Share on other sites
Quote:
 Original post by TrapThe 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 TrapIn 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)?

##### Share on other sites
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.

##### Share on other sites
Quote:
 Original post by TrapDependant 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?

##### Share on other sites
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.

##### Share on other sites
Quote:
 Original post by TrapThere 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.

##### Share on other sites
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.

1. 1
2. 2
JoeJ
17
3. 3
4. 4
frob
11
5. 5

• 13
• 16
• 13
• 20
• 13
• ### Forum Statistics

• Total Topics
632181
• Total Posts
3004625

×