Name: Anonymous 2018-10-12 17:08
So, why are you not using dependent types yet? Do you like your programs randomly crashing?
and a crash is what I need to determine something has gone wrong.Dependent types help you find logical errors in your program, such as divisions by 0 and possible out of bounds accesses. Why would you need to wait until runtime in order to find a bug in your program? There are many released and supposedly stable programs in production that have passed testing and still have all kinds of bugs (including security bugs) that could have been prevented by dependent types.
List 50 Int for the type of a list with 50 elements. A functions like head that take the 1st element of a list could have a type like {t : Type} -> {length : t} -> (value : t) -> List (1 + length) t -> thead (cons 9 nil) = 9head nil = compile time type error as the type of nil is something like List 0 Intint sussman[10]; sussman[90] = 100; so it helps with array index out of bounds stuffNot only, you can even use it to avoid divisions by 0, as well as implement type-safe printfs. All kinds of things that have to do with safety and correctness really.
how is this different from just exception handling where you make sure something isn't out of bounds?That this checks if your program is correct at compile time. You get an exception at runtime - possibly crashing your program.
You're still going to have a conditional branch in the machine code.Yes, did anyone tell you otherwise?
The idea is basically that types may depend on values, so you can have something like List 50 Int for the type of a list with 50 elements.Then C got dependent types:
That way you basically can't do things like int sussman[10]; sussman[90] = 100;
typedef int dependent_type[50];
dependent_type A;
#include <stdio.h>
int main(){A[90]=100;printf("%d",A[90]);;}int main(){A[90]=100;printf("%d",A[90]);;}Now try
int main(){int i; scanf("%d\n", &i); A[i] = 100; printf("%d\n", i);}printf("%d\n", A[i]); Type safe division: https://gist.github.com/edwinb/0047a2aff46a0f49c881I can just
catch ZeroDivisionError in other langs to achieve the same exact thing. the same exact thing"Data loss" and "crashing on runtime" is not the exact same effect as "catching a possible error at compile time".
print "Attempt to divide by zero!", which is literally no different than catching the exception and doing that.instead of crashing, in Idris you have, print "Attempt to divide by zero!"You have to use
choose only on user input. For non-user input you might not need to do that (so you will not need to have any print "Attempt to divide by zero!").which is literally no different than catching the exception and doing thatExcept that you might forget to catch said exception. "b-buuut the compiler will warn me!" - what if you pass a provably non-zero divisor? You will have to still catch the exception, which is retarded.
sizeof array / sizeof *array instead - which does not work correctly for pointers), along with no warning if one is incorrect or missing. for freeThats a lie. Garbage collection, performance, long compile times and complexity of implementation.
Garbage collectionNot more necessary than any language.
performanceType checking happens only at compile time, in fact it has the opportunity of being faster since you do not need to check if your arguments are null everywhere.
long compile timesFaster than C++. And it's not like compile times really matter, you are not going to recompile the whole project every time you make a change - only the file(s) that you changed.
complexity of implementationI have implemented a dependent type system in 100 lines of code. Pretty sure that this is less than even the type system of the average C implementation or haskell.
I have implemented a dependent type system in 100 lines of code.Extraordinary claims require extraordinary evidence.
shows paper clearly lacking code and clearly not written by him"I have implemented a dependent type system in 100 lines of code."
where it is"Its...in the paper..somewhere.."