• Advertisement
Sign in to follow this  

Unity What is 'dependent typing'?

This topic is 4722 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
  • Advertisement
  • Popular Tags

  • Advertisement
  • Popular Now

  • Similar Content

    • By Vu Chi Thien
      Hi fellow game devs,
      First, I would like to apologize for the wall of text.
      As you may notice I have been digging in vehicle simulation for some times now through my clutch question posts. And thanks to the generous help of you guys, especially @CombatWombat I have finished my clutch model (Really CombatWombat you deserve much more than a post upvote, I would buy you a drink if I could ha ha). 
      Now the final piece in my vehicle physic model is the differential. For now I have an open-differential model working quite well by just outputting torque 50-50 to left and right wheel. Now I would like to implement a Limited Slip Differential. I have very limited knowledge about LSD, and what I know about LSD is through readings on racer.nl documentation, watching Youtube videos, and playing around with games like Assetto Corsa and Project Cars. So this is what I understand so far:
      - The LSD acts like an open-diff when there is no torque from engine applied to the input shaft of the diff. However, in clutch-type LSD there is still an amount of binding between the left and right wheel due to preload spring.
      - When there is torque to the input shaft (on power and off power in 2 ways LSD), in ramp LSD, the ramp will push the clutch patch together, creating binding force. The amount of binding force depends on the amount of clutch patch and ramp angle, so the diff will not completely locked up and there is still difference in wheel speed between left and right wheel, but when the locking force is enough the diff will lock.
      - There also something I'm not sure is the amount of torque ratio based on road resistance torque (rolling resistance I guess)., but since I cannot extract rolling resistance from the tire model I'm using (Unity wheelCollider), I think I would not use this approach. Instead I'm going to use the speed difference in left and right wheel, similar to torsen diff. Below is my rough model with the clutch type LSD:
      speedDiff = leftWheelSpeed - rightWheelSpeed; //torque to differential input shaft. //first treat the diff as an open diff with equal torque to both wheels inputTorque = gearBoxTorque * 0.5f; //then modify torque to each wheel based on wheel speed difference //the difference in torque depends on speed difference, throttleInput (on/off power) //amount of locking force wanted at different amount of speed difference, //and preload force //torque to left wheel leftWheelTorque = inputTorque - (speedDiff * preLoadForce + lockingForce * throttleInput); //torque to right wheel rightWheelTorque = inputTorque + (speedDiff * preLoadForce + lockingForce * throttleInput); I'm putting throttle input in because from what I've read the amount of locking also depends on the amount of throttle input (harder throttle -> higher  torque input -> stronger locking). The model is nowhere near good, so please jump in and correct me.
      Also I have a few questions:
      - In torsen/geared LSD, is it correct that the diff actually never lock but only split torque based on bias ratio, which also based on speed difference between wheels? And does the bias only happen when the speed difference reaches the ratio (say 2:1 or 3:1) and below that it will act like an open diff, which basically like an open diff with an if statement to switch state?
      - Is it correct that the amount of locking force in clutch LSD depends on amount of input torque? If so, what is the threshold of the input torque to "activate" the diff (start splitting torque)? How can I get the amount of torque bias ratio (in wheelTorque = inputTorque * biasRatio) based on the speed difference or rolling resistance at wheel?
      - Is the speed at the input shaft of the diff always equals to the average speed of 2 wheels ie (left + right) / 2?
      Please help me out with this. I haven't found any topic about this yet on gamedev, and this is my final piece of the puzzle. Thank you guys very very much.
    • By Estra
      Memory Trees is a PC game and Life+Farming simulation game. Harvest Moon and Rune Factory , the game will be quite big. I believe that this will take a long time to finish
      Looking for
      Programmer
      1 experience using Unity/C++
      2 have a portfolio of Programmer
      3 like RPG game ( Rune rune factory / zelda series / FF series )
      4 Have responsibility + Time Management
      and friendly easy working with others Programmer willing to use Skype for communication with team please E-mail me if you're interested
      Split %: Revenue share. We can discuss. Fully Funded servers and contents
      and friendly easy working with others willing to use Skype for communication with team please E-mail me if you're interested
      we can talk more detail in Estherfanworld@gmail.com Don't comment here
      Thank you so much for reading
      More about our game
      Memory Trees : forget me not

      Thank you so much for reading
      Ps.Please make sure that you have unity skill and Have responsibility + Time Management,
      because If not it will waste time not one but both of us
       

    • By RoKabium Games
      We've now started desinging the 3rd level of "Something Ate My Alien".
      This world is a gas planet, and all sorts of mayhem will be getting in our aliens way!
      #screenshotsaturday
    • By Pacoquinha Studios
      Kepuh's Island is Multiplayer 3D Survival Game where you survive on the Kepuh's Islands, confronting challenges that are not only other players but also bosses, and even the environment itself.
      We have a lowpoly faster battle-royale idea, where about 12 players on the map fighting for survival! Also adding some more things into that style such as bosses around the map giving you abilities and much more such as vehicles, weapons, skins, etc...
      Now we are on cartase which is a crowdfunding online which purpose is to raise funds for the development of the game. Come and be part of this development.
      Link for Cartase: https://www.catarse.me/kepuhsisland?ref=project_link
      We post updates and trailers on
      Twitter: https://twitter.com/pcqnhastudios
      Facebook: https://www.facebook.com/pacoquinhastudios/
      Site: http://pacoquinhastudios.com.br
      If you could check out it would be great
      Thnks
      Some images:





  • Advertisement