Dependent types and totality

Whoever the fuck ever came up with the brilliant idea that all dependently-typed languages must be total? This is totally retarded, having to prove termination of everything. And it's totally unnecessary

Their only argument is "uh, you know, muh typechecking, it becomes undecidable". Guess what, dipshits, people have been running code whose termination is undecidable for decades. No one is afraid of non-terminating loops at runtime, so how can non-termination at compile-time be a problem? You run the typechecker, it crashes with an overflow/segfault/whatever, you edit your code and then it compiles. But nooo, these cretins believe that this is impossible and you have to only use total functions in types, and then prove that they terminate via structural recursion. Fucking academic numbskulls.

Now, of course totality is essential for proof assistants. But dependently typed languages are not all proof assistants! Dependently-typed languages can be Turing-complete with a Turing-complete, undecidable type system! Why don't these retards realize this?

Why use a special language?
Just write a program to test if an arbitrary program completes or loops forever.
Run that instead.

Whenever I see unary numbers (aka Peano numerals), I want to throw up. They are literally a disgrace to the dependent types community. Hell, even assembly programmers have it binary, and only totality morons are stuck with unary to prove termination of even the most trivial functions. No fucking way.

if you can write an infinite loop in a language it will have a type like this f : forall a. Int -> a.

It is easy to prove anything you want from this, for example: f 3 : String = Int.

Now you can unsafeCoerce a String into an Integer causing malformed data.

That is why a dependently typed language should be total.

>>4
Isn't unsafeCoerce the problem there though? Not that I know what that really does, it just doesn't sound safe.
And what about raise : exn -> 'a? Did >>1 really mean

muh type inference, it becomes undecidable

?

>>4
Not every dependently typed language has to be a proof assistant. In terms of your example: since f : forall a. Int -> a is an infinite loop, using it in type-level calculations will cause the typechecker to crash. Hence you would never run your program because you wouldn't even be able to compile it. Thus it's perfectly okay to have a Touring-complete dep-type language.

>>5
Type inference becomes undecidable in dep-typed languages with or without totality. It's a given.

>>6
That is not how typechecking works

>>7
Why not? It's the only way to do it once you go into the undecidable realm. Prove what you can, fail to prove what you can't.

Is /prog/ unique for having a regular thread about dependent type theory, is it just becoming hip now and its also on the other programming discussion forums that I don't browse?

Dependent Types and Totality is the new Object-Oriented cult ideology. If you trace their histories carefully, both have their roots in Jewish Marxism and Jewish Set Theory.

Jewish Set Theory.

infinity
afterlife

Aryan Atheism

finity
no afterlife

Now who is more desirable?

>>7
That's the way pretty much all of software has worked for decades. Nobody proves termination of programs before running them. They just run it. And if there's a segfault/overflow because of an infinite loop - well, people just rewrite the program and run it again. No need to prove every fucking step.

In fact, there is a theorem about total languages that states: proving all your shit has some real, real bad worst cases, like exponentially bad (in the size of the program). Total languages suck.

https://existentialtype.wordpress.com/2014/03/

>>11

Aryan Atheism

Bitch, please. Aryans had polytheism, not atheism.

>>9
its been hip for a while. it's kinda depressing.. the haskell guys mostly hyped it up to kids who wanted to prove they were smart.

>>14
That's fucking sad.

So are there any real reasons against a Touring-complete dependent type language, or not?

>>16
it will be inconsistent and useless and/or go into an infinite loop when you try to typecheck your code.

>>17
Infinite loops during typechecking are not a problem.
Any program that compiles will be consistent.
Useless? Obviously not.

So, there are no reasons not to create a Turing-complete dep-type language.

>>18
There are no reasons to create one either.

>>19
Sweet, sweet dependent types are reason enough.

>>17,19 is the anticudder.

Ada is not total and has (limited) dependent types.

(defmacro hang-compilation () (loop))