How many times were dependent types invented in parallel? Fascinating how many languages had limited notions of dependent types before realizing they were limited notions of dependent types. Particularly common in the history of OO languages
Conversation
Not thinking of path-dependent types in Scala, though those are for sure a great introduction to a limited but very useful notion of dependent type in an actual mainstream language, especially for folks with OO programming background:
3
2
8
But rather a friend pointed to predicate object types in Cecil, dating back to the 1990s, which look suspiciously like a cute gradual limited form of dependent type: projectsweb.cs.washington.edu/research/proje
1
6
Static checking happened by way of annotations, which one can view as a form of proof object, but the annotations were only dynamically enforced rather than statically checked themselves
1
3
Just interesting. I think it's funny that people think of dependent types as weird and niche, but keep inventing them over and over again. They're going to be everywhere eventually in at least limited forms, with better understanding informing better implementations and tools
1
2
16
I mean that. I really think they'll leak into languages the way polymorphism did. At first in totally ad hoc ways, then reconciling with the theory and implementing in much more elegant ways
2
8
I still don't understand the difference between dependent types and what you can get with C++ templates - other than they aren't total hacks and you don't need Circle-lang to automate functions on them. 😅
1
They are close but there are some differences. Templates are limited to compile time instantiation, where as application in dependently typed languages can happen at any stage (compile time or run time). This is useful for code generation, but limits expressiveness.
For example you can't have templates that depend on runtime values in C++, which can be super useful for ensuring you are correctly handling user input, for example.
1
In dependent types, function application is type checked ahead of time - in C++'s templates instantiations can fail if the template expands to invalid code. IIRC there's some type checking for non-type template parameters, but instantiation can still induce expansion failure.
1
Show replies