# Unity What is 'dependent typing'?

This topic is 4821 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.

• 10
• 17
• 9
• 14
• 41
• ### Similar Content

• I have already chosen my favorite from the concept artist which one do you like better 1 2 or 3?

Also still looking for a writer and a 3d artist message if you are interested!

• Hey There,
I am a developer and Im working on a blockchain based infinite runner type game. Right now, I am working on releasing the beta version with a couple other game developers, but would love to expand the team and have other talented and bright people contributing. The game portion of the project isnt very complicated, and wouldnt require anyone to pull thier hair out for it.
If you are interested in joining a project, interested in the idea, or would like some more information, please don't hesitate to ask either by commenting, discord (username: Guppy#7625), or by email (armaangupta01@gmail.com).
Thank you!

• I am trying to build a particle system for unity based on "Destiny particle architecture " released in Siggraph.
I encounter a problem in trying to understand how they iterated this:

Converted to spline function and the result is

i wanted to know how did they converted the function in the editor to represent the graph ??

• This is my first experiment use for create my original character little cute dragon chibi use zbrush and blender and use unity3d assest free for enviroment scene you have feedback?

• By Aryndon
Project Redemption is an semi-fantasy RPG with a linear story and an elaborate combat system.
We are building in Unity and are currently looking animators and artists.
What we are looking for
-Someone who is okay with split revenue/profits when finished
-Collaborate with others in the team. Do you have an idea/thought on what should be included? Tell us!
-Someone who wants to work with people that are passionate about this project
If you are interested. Please message me and I will get back to you as soon as possible! Or add me on Discord AJ#6664