Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

explain dependent types to someone who primarily uses java

Use Internet Explorer to ask the AI Mind about dependent types:

http://ai.neocities.org/FirstWorkingAGI.html

Maybe because computers have a finite number of registers, accessible addressing space, and physical limitations, and a crash is what I need to determine something has gone wrong.

>>2
Thinking about or in terms of Java is painful.

>>3
Internet explorer does not work on Debian.

>>4

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.

>>5
if you can't explain it to someone who isn't familiar with it, you don't really understand it yourself

I didn't say you have to explain it in terms of java, just that I am not familiar with languages that use dependent types

>>6
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. 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 -> t
(the arguments in {} can automatically be deduced by the compiler)
And you get:
head (cons 9 nil) = 9
head nil = compile time type error as the type of nil is something like List 0 Int
That way you basically can't do things like int sussman[10]; sussman[90] = 100;

>>7
so it helps with array index out of bounds stuff, but can you give some specific real-world examples of when/where you'd use this?

how is this different from just exception handling where you make sure something isn't out of bounds?

>>8

so it helps with array index out of bounds stuff

Not 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.

Someone explain to me how the fuck you can check bounds purely at compile time. Let's say the array is user input. Yeah good luck buddy. You're still going to have a conditional branch in the machine code.

>>10

You're still going to have a conditional branch in the machine code.

Yes, did anyone tell you otherwise?
The point is that the compiler will tell you if you forget said conditional (due to the types not matching), dumbfuck.

>>11
Then why not use Python, Java, etc. which already do that but without the extra bookkeeping of types?

>>12
Except that they do not. None of these languages will warn you at compile time for such violations.

>>3

https://github.com/PriorArt/AGI/blob/master/ghost.pl

Good lord, this is awful code

>>7

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:
typedef int dependent_type[50];
dependent_type A;

That way you basically can't do things like int sussman[10]; sussman[90] = 100;

gcc -Wall -pipe -O3 dep.c
typedef int dependent_type[50];
dependent_type A;
#include <stdio.h>
int main(){A[90]=100;printf("%d",A[90]);;}
dep.c: In function ‘int main()’:
dep.c:4:16: warning: array subscript is above array bounds [-Warray-bounds]
int main(){A[90]=100;printf("%d",A[90]);;}

>>15
-Werror -Wfatal-errors will halt compilation on any errors/warnings
gcc -Wall -Werror -Wfatal-errors -pipe -O3 dep.c

dep.c: In function ‘int main()’:
dep.c:4:16: error: array subscript is above array bounds [-Werror=array-bounds]
int main(){A[90]=100;printf("%d",A[90]);;}
^
compilation terminated due to -Wfatal-errors.
cc1plus: all warnings being treated as errors

>>15

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);}
It will compile just fine.

*printf("%d\n", A[i]);

Type safe division: https://gist.github.com/edwinb/0047a2aff46a0f49c881
Type safe printf: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292

>>19

Type safe division: https://gist.github.com/edwinb/0047a2aff46a0f49c881

I can just catch ZeroDivisionError in other langs to achieve the same exact thing.

>>20

the same exact thing

"Data loss" and "crashing on runtime" is not the exact same effect as "catching a possible error at compile time".

marathon = runtime
bukkake = cum pile time

>>21
all the Idris code does is force you to check if the divisor is 0, as if all division procedures in other languages don't already check if the divisor is zero. instead of crashing, in Idris you have, print "Attempt to divide by zero!", which is literally no different than catching the exception and doing that.

tl;dr the emperor has no clothes

>>23

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 that

Except 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.
Also, try to think of it from another way: what if you are dividing by a value that you think that will never be 0 but in reality it might be 0? You will simply not get any compile time warning that you fucked up in languages with non-dependent types.

>>17
A C program will probably include a runtime check to avoid that. Like if(index >= sizeof(array)){deny}

>>25
"Probably" - except if it is one of the many programs that do not, or have an incorrect one (such as heart-bleed or such as your very own example - I think you mean sizeof array / sizeof *array instead - which does not work correctly for pointers), along with no warning if one is incorrect or missing.

>>26
This can be predefined
const int MAX_INDEX_OF_F=20;
#define MAX_INDEX_OF_F 20
if(index >=MAX_INDEX_OF_F)

Sure, but it just shows how easy it is to fuck up - something that languages with dependent types stop for free.

>>28

for free

Thats a lie. Garbage collection, performance, long compile times and complexity of implementation.

>>29

Garbage collection

Not more necessary than any language.

performance

Type 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 times

Faster 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 implementation

I 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.

Proof for how easy it is to implement it: https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

>>30

I have implemented a dependent type system in 100 lines of code.

Extraordinary claims require extraordinary evidence.

>>32
See >>31

>>33
Thats not code, its a theoretical paper and much larger than 100 lines.

CoC's inference rules, you must be a mental midget to need more than 100 lines of code to implement them https://en.wikipedia.org/wiki/Calculus_of_constructions#Inference_rules_for_the_calculus_of_constructions

>>34
It is not a theoretical paper, it is a practical tutorial.

>>35
Burden of proof is on you, you claim that "I have implemented a dependent type system in 100 lines of code." Sophistry about mental midgets is irrelevant.

>>36

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.."

>>38
Whom art thou quoting?
I never said that I will post my implementation.
Apparently though you are too stupid to look for one by yourself https://gist.github.com/ChristopherKing42/d8c9fde0869ec5c8feae71714e069214

>>39
So its essentially:
1.A fairly normal C++ Class Template
2.The setter function filters incoming values by an internal parameter(such as size or something).
3.A getter function throws exception(Nothing) if something outside of range is requested.
What is so revolutionary about this?

>>40
That none of what you just described happens at compile time.

>>41
>>17 happens at runtime.

>>42
Yes, >>17 crashes at runtime instead of warning you at compile time, which is my point.

>>43
How >>17 would behave at compile time with dependent types? C++ version with setters/getters on protected boxed value would work fine at runtime.

>>44
It would complain that the type of the array is something like Vect n Int while the head function requires a value of type Vect (n + 1) Int

C++ version with setters/getters on protected boxed value would work fine at runtime

The issue is that the compiler will not warn you if you forget or mis-implement said getters/setters. See >>24

>>45

while the head function requires a value of type Vect (n + 1) Int

In that case dependent types are safer.
Its likely possible within the class to add static_assert or exotic set of constexprs to fail template instantiation, but your argument is that the programmer can also fuck up the static_assert/constexpr's too. There is however a modern alternative to this, C++ concepts:

C++ concepts can be enabled in gcc with -fconcepts and is probably the closest thing to implementing dependent type
https://gcc.gnu.org/onlinedocs/gcc/C_002b_002b-Concepts.html

>>46
Concepts seems like some form of proof checker or something, which is somewhat close to dependent types indeed - seems similar to what F* uses.
But I might have just misunderstood what concepts are about, this seems like a new thing.

>>47
Its just advanced syntax sugar for static_assert on constexpr's which takes template parameters or other constexpr's.
See https://en.cppreference.com/w/cpp/language/static_assert

https://www.boost.org/doc/libs/1_48_0/libs/concept_check/using_concept_check.htm
Boost had this before current_year C++ standards

The future C++20 standard has concepts(aka constraints), but its still not adopted by all compilers, support is poor except GCC.
https://en.cppreference.com/w/cpp/language/constraints

#define STATIC_ASSERT( compile_time_expr ) typedef char __STATIC_ASSERT__[( compile_time_expr )?1:-1];

>>50 The Virgin constraint
>>51 the Chad impossible array

>>45
Would that also mean scanf equivalent function needs to implement handling dependent types as output?
How would this look in idris?

>>53

Would that also mean scanf equivalent function needs to implement handling dependent types as output?

No

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
template<typename T,size_t size> class contain {private: T arr[size];
public:
T operator [](size_t i) const{
if(!(i<size)){puts("Requested Index out of range. Aborting");exit(2);}
return arr[i];};
T& operator[](size_t i) {
if(!(i<size)){puts("Input Index out of range. Aborting");exit(1);}
return arr[i];};};

int main(){
contain<int,50> A;
int i;
int rts=scanf("%d", &i);
A[i] = 100;
printf("%d", A[i]); return rts;} Edited on 15/10/2018 04:53.

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
template<typename T,int size> class contain {private:	T arr[size];
template<typename T,size_t size> class contain {private:	T arr[size];
public: 
T operator [](size_t i) const{
if(!(i<size)){puts("Requested Index out of range. Aborting");exit(2);}
return arr[i];};
T& operator[](size_t i) {
if(!(i<size)){puts("Input Index out of range. Aborting");exit(1);}
return arr[i];};};

int main(){
contain<int,50> A;
int i;
int rts=scanf("%d", &i);
 A[i] = 100;
 printf("%d", A[i]); return rts;}

>>54
In that case what the program will do on invalid input?

>>54
Lets reiterate:
1.Scanf-equivalent outputs integers
2. ...
3.Dependent type accept only restricted subset of integers.
What is happening at #2

>>55
Hi FrozenANUS

>>55
Someone did not read the thread, huh? See >>45

>>56
Whatever the programmer chose.

>>57
2. The programmer verifies that the input is correct and in such a case passes it to the function.

>>59
Why should I have to verify the input? That's the computer's job.

>>60
...
What?

>>61

The programmer verifies that the input is correct

Why doesn't the computer do it?

>>62
Could you explain clearly what you mean by that please?

all input should be verified server-side

client-side input validation is not secure

>>63
I assume he wants for dependent types(proof checker) to verify input too. Removing the manual check("The programmer verifies that the input is correct") from the program.

>>65
lmao @ you thinking ``muh dependent types'' will solve ALL input validation issues ever

it's not that simple, buddy

>>66
What makes you think that?

>>67
if it was so simple, we'd have done it by now

why would corporations who stand to lose a lot by getting hacked avoid something that would make them hack-proof? because it's not a magic bullet like you say it is, that's why

>>68

if it was so simple, we'd have done it by now

But we have.

why would corporations who stand to lose a lot by getting hacked avoid something that would make them hack-proof?

Because it is cheaper to hire Indians for pennies who have no idea about dependent types than hire people with some CS background. Why do you think that crap like Windows and Java are so popular?

There’s no way you can encode all the logic to sanitize input in just types.

B-b-but you can write code that output types!

But I can also directly write that code without types as a middleman.

>>70

There’s no way you can encode all the logic to sanitize input in just types.

What makes you think that? Haven't you heard of Curry–Howard isomorphism?

But I can also directly write that code without types as a middleman.

Code that you can't prove that is correct, sure. This is why most programs nowadays are unstable and full of vulnerabilities.

>>69
this guy thinks he has security 100% figured out

kek dude, you don't even know what you don't know

>>72
Please do feel free to correct me. Can you?

>>73
https://www.exploit-db.com/
https://www.cvedetails.com/
you remind me of the ``infinite compression'' thread
you think complex problems have super simple solutions and that they're already solved, which is not the case

>>74

https://www.exploit-db.com/
https://www.cvedetails.com/

All I see are bugs in software written in C and Java, neither of which have dependent types.

which is not the case

What makes you think that in this specific case?

>>75
cybercrime causes billions of dollars in damages every year, and you, posting on a low-traffic textboard, claim to know the solution

if you really knew a solution, you should try to profit off it

or, more likely, you're just talking out of your ass, and security is a little more complicated than mere dependent types, because you don't know shit about infosec

will dependent types stop someone from clicking on a link? will it stop SQL injection? will it stop word docs/maldocs/macros? will it stop JS embedded in PDFS? will it stop ransomware? will it stop cryptojacking? will it stop keylogging? will it stop RATs? will it stop XML external entity attacks? will it stop reflected XSS? DOM XSS? CSRF? remote file inclusion? local file inclusion? billion laughs? UDP reflection? UDP amplification? NTP reflection? default passwords? overflows? numeric underflows? slowloris resource exhaustion? predictable session tokens? predictable resource location? sybil attacks? hash cracking? social engineering? covert channels? data exfiltration? privilege escalation? reverse shells? steganography? file descriptor attacks? vlan hopping? arp spoofing? shatter attacks? SSRF attacks? cache poisoning? DNS hijacking? DHT poisoning? CTS flooding? smurf attacks? fraggle attacks? format string vulnerabilities? array indexing errors? mismatched array new/delete? stack overrun? unused values? file handle leaks? OSINT/opsec issues? predictable TOTP? dns exfiltration? exfil via x.509 metadata fields? content-type header injection? WMI hijacking? UEFI rootkits? network resource leaks? debug features left on in production? compiler backdoors? ephemeral netcat backdoors? hardware backdoors? side channel analysis? rowhammer bit-flipping? van eck phreaking? null pointer dereferencing? uninitialized/improperly initialized memory? lack of proper ASLR? checksum collisions? port knocking? clickjacking? DNS sinkholing? remote code execution? VM escapes? missing lower bounds? iterator invalidation of mutable data structures leading to undefined behavior? data inferrence? misconfiguration? directory enumeration? unhandled return codes? hooking? return pointers to local variables? invalid use of negative values? passing large parameters by value? underallocations of dynamic data? nop sleds? heap spraying? heap pointer replacement? JIT spraying? race conditions?

there are hundreds and hundreds of other attack vectors I know about that I could post but it's late and I'm drinking and need to fall asleep soon

>>76
Most of these have nothing to do with programming languages themselves. Some of them in fact are physics related (van eck phreaking) or people related (social engineering). This thread is about dependent types solving bugs in software.

privilege escalation?
overflows? numeric underflows?
null pointer dereferencing? uninitialized/improperly initialized memory?
format string vulnerabilities? array indexing errors? mismatched array new/delete? stack overrun? unused values?
remote code execution?
iterator invalidation of mutable data structures leading to undefined behavior?
unhandled return codes?
return pointers to local variables? invalid use of negative values?
underallocations of dynamic data?

Yes, dependent types protect against these.

file handle leaks?
network resource leaks?
race conditions?

Pretty sure that you need linear types for these.

There are probably some that I missed.

>>1

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

What if NPCs are incapable of writing safe code by design? They lack the level of abstract thought required to imagine the code being exploited. They just write code as requested by design and wonder why it randomly crashes and allows exploits.

>>78
I once contributed to an open source project (game) where the leader was incapable of considering his ideas being exploited against his vision.
It was pain.

Average software quality will be greatly improved and even programmers who write 99% safe code will benefit. Even C++ concepts-lite that is being discussed to inclusion in C++20 will change the industry.

>>80
people said the same thing about rust and go, but look what happened as a result

pretty much nothing

>>77
I'm just saying there's more to security than dependent types
many security issues aren't about language design
it's like saying access modifiers are the difference between a secure or insecure program lol

>>79
Please post about it.

>>81
Nobody said that about go and many supporters of dependent types raised their concerns when Rust appeared.

>>82
We are talking about software security here. Why are infosec people so dumb?

>>83
software security is more than just language design, a lot of it is what you do within the language

>>84
Yes, and dependent types filter out a lot of common errors when programming.

>>83

Please post about it.

It was mostly vidya logic, so not very /prog/ relevant. Shit like not realizing that bumping numbers without touching the underlying mechanics will just lead to more tedious kiting.

It's just that mentality of

I did something therefore it's fixed, thread over, issue closed, working as intended

that is impossible to work with. With those people, you have to convince them emotionally, by licking their asses and trying to sneak your ideas as theirs.

>>86
What project was that?

Bump

>>87
CDDA

>>89
The roguelike?

>>90
Yes

>>77
how the fuck do dependent types prevent priv-esc? do you even know what it is?

>>92

how the fuck do dependent types prevent priv-esc?

trivially

>>93

>>93
your're are an anus

>>93
if it's so trivial then explain it to me, anus

>>96
Give me an example and I will tell you how to prevent it with dependent types.

>>97
Prevent those dubs

Dubs

>>99
nice dubs

>>97
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus). but OK, I'll explain it to you:

priv-esc is not an attack method. it's a consequence of an attack: one user (normally a low-privileged one) can execute code as another (normally high-privileged). usually, it's done by exploiting a process running with desired privileges (so things like buffer overflows and injections, but also logic bugs and race conditions which cannot be trivially prevented by a type system), but it can also come from exploitation of bad OS-level configuration - e.g. parameter injection through shell expansion, world-writeable suid binaries/scripts, world-writeable (and overly powerful) configs etc. Edited on 22/11/2018 11:26.

>>97
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus) who doesn't know what he's talking about. but OK, I'll explain it to you:
stop moving goalposts, anus. first you said that it can be trivially prevented, now you say that I must give you examples. this once again proves that your're are speaking out of your're are anus (recursively, because your're are an anus). but OK, I'll explain it to you:

priv-esc is not an attack method. it's a consequence of an attack: one user (normally a low-privileged one) can execute code as another (normally high-privileged). usually, it's done by exploiting a process running with desired privileges (so things like buffer overflows and injections, but also logic bugs and race conditions which cannot be trivially prevented by a type system), but it can also come from exploitation of bad OS-level configuration - e.g. parameter injection through shell expansion, world-writeable suid binaries/scripts, world-writeable (and overly powerful) configs etc.

>>101

buffer overflows and injections

Can be prevented by dependent types.

but also logic bugs

Can also be prevented by dependent types.

and race conditions

You probably need linear types for that.

>>102
buffer overflows and injections can be prevented by dependent types (although it's harder for injections as they usually happen on the boundaries of languages - e.g. calling shell from C or SQL from PHP). logic bugs only theoretically can, but that's equivalent to formally proving a program - which is never trivial and can't be done in general case (because of halting problem).

of course you conveniently ignored how priv-esc can happen by exploiting OS-level stuff. lets see these guys implement diff dependent types prevent that

>>103

although it's harder for injections as they usually happen on the boundaries of languages

You could have a dependent type like system : (s : string) -> doesNotContainUnescapedQuotes s = True -> IO ()

logic bugs only theoretically can

Buffer overflows are also logic bugs.

can't be done in general case (because of halting problem).

Nice meme

by exploiting OS-level stuff

Dependent types can't prevent bugs in other programs.

>>104

doesNotContainUnescapedQuotes

that might be the only way to prevent shell injection but it's an anus-backwards approach when it comes to SQLi. the correct solution is not treating SQL queries as strings. see: parametrized queries.

Buffer overflows are also logic bugs.

buffer overflows aren't really what security people would call logic bugs. this term refers to unintended consequences of a program's high-level design, not low-level details about programming language, calling convention and the processor architecture.

Nice meme

dependent types solve halting problem?

Dependent types can't prevent bugs in other programs.

how would they prevent those bugs if an OS was written in a dependently typed language? that's a clear example of what I mean by 'logic bugs'

>>105

dependent types solve halting problem?

Languages with dependent types tend to not be Turing complete. Moreover the halting problem is irrelevant for just about anything.

how would they prevent those bugs if an OS was written in a dependently typed language?

Formal verification

>>106

Languages with dependent types tend to not be Turing complete.

lets see these guys implement diff a kernel

Formal verification

which is non-trivial, time-intensive and doesn't even require dependent types. you can look at any bug and say '100k additional man-hours by guys with PhDs would have prevent it', but that's not saying much.

meme