Jump to content
  • Advertisement
Sign in to follow this  
CoffeeMug

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.

If you intended to correct an error in the post then please contact us.

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 this post


Link to post
Share on other sites
Advertisement
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 this post


Link to post
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 this post


Link to post
Share on other sites
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 elements
SmallList : lists where size is <= 3 elements
l = [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 this post


Link to post
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 this post


Link to post
Share on other sites
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?

Share this post


Link to post
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 this post


Link to post
Share on other sites
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.

Share this post


Link to post
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.

Share this post


Link to post
Share on other sites
Sign in to follow this  

  • Advertisement
×

Important Information

By using GameDev.net, you agree to our community Guidelines, Terms of Use, and Privacy Policy.

We are the game development community.

Whether you are an indie, hobbyist, AAA developer, or just trying to learn, GameDev.net is the place for you to learn, share, and connect with the games industry. Learn more About Us or sign up!

Sign me up!