(untitled)

Is anyone else here into type theory? I find it extremely depressing how pretty much every popular language decided to disregard pretty much all research into the topic.(USER WAS WARNED FOR THIS POST, You should always elaborate on your opinions rather than just spilling the soykaf.)

Does type theory even have any practical applications outside of automated theorem proving?

>>38357 Manual theorem proving + using it in programming

You might find Prolog interesting. Outside of that i had the impression its a topic for compiler construction so most people wont touch it.

theres not really an easy way into it if you are NOT in college for math like im a highschool drop out. i only know some finite set theory

>>38356 >type theory Is it an attempt to create set theory by philosopher Russel?

people at edinburgh uni are obsessed with it for some reason

Been getting more and more invested in using it in my programming, and at this point i would be rather annoyed without it. Distinct mappings of scalars and simple vector types into higher order logical types helps tremendously in reducing bugs and making better systems. Not to mention better usage of sum and product types to better represent how a value should be treated. I know that only scratches the surface, I am only a beginner in the theory behind it all. But even with that preliminary knowledge it has improved my code quality and software quality significantly. I think too many programmers try and tie themselves into something more "tangible", they call themselves engineers after all. As such, mainstream languages want to limit the amount of abstract knowledge required to actually be used, since it alienates 90% of programmers who would rather play with the new AWS product than better their knowledge of computing.

>>38378 Huh, that sounds almost too good to be believable. Can you recommend books or papers? Or any type theory book for undergrads will suffice?

Do you have examples of how popular languages disregard all research? I had a type theory class in college. It was a while ago, but I remember Java exemplified some of the least intuitive results brought up. I also know new research had to be carried out to design some Rust features properly. But yeah, other than that, I never really had to use it other than for toying around with proof assistants.

Because type theory is a mix of obvious things with snake oil grade bullshit.

>>38378 >I think too many programmers try and tie themselves into something more "tangible", they call themselves engineers after all. As such, mainstream languages want to limit the amount of abstract knowledge required to actually be used, since it alienates 90% of programmers who would rather play with the new AWS product than better their knowledge of computing. This. If we want maintainable and readable code I think mathematics is kind of the golden standard. Obviously programming requires a slightly different approach (you can't just call everything x or some Greek char) but the "high level" declarative approach seems much more suited for humans than the imperative (sometimes machine dependent) approach. But the imperative paradigm is seen as more tangible and I think programmers are shooting themselves in the foot by always reaching for the "tangible" solution. Imperative code often requires significant attention to detail which is easy for a human to overlook. Generally, I would much rather have a machine translate declarative code to imperative code because machines don't make mistakes just because something is tedious. Another benefit is that you don't have to focus on the inessentials like memory management, instead you're fully immersed in the problem domain. A little bit of knowledge about typed lambda calculus goes a long way but watch ppl's faces contort in disgust if you even mention "currying" let alone "type variable" or anything along those lines.

>>39112 People do manual optimizations because tools doing equally well are harder to write than manual hacks.

>>38356 Sum and product types are useful, and existential quantification is great, but what more do you need? I think some of the properties of type theory aren't even that useful for programming. An unsound type system is easier for writing computer programs even if it can't be used for formal proofs.

>>39131 >[...] and existential quantification is great, but what more do you need? That is already more than what most popular languages give you. Not to mention that what they do in fact give you is unbelievably ad-hoc and obese

>>38356 are you familiar with upper semantic layer languages ?

>>38356 I mean... what's the alternative, rich assholes paying their corpodrones to invade your hobby? You're either dumb or need to widen your horizons as to who you could be hanging with (IF <conditions>). No I'm not into type theory but I'll probably learn the basics in the progress of learning more lambda calculus... I suspect it'll help with focusing in automatic proof search.

>>38356 If you look at what people do and not what they say you'll find that no one cares about language design at all. They just use the language that has libraries written for it. Python is the best example, horribly designed, dynamically typed, etc. Golang is also really poorly designed. I will give it credit, its standard library is pretty good, and the tooling is nice and simple. But then you realize it didn't have generics for 10 years when it had generics for maps. (why?) Even at large corporations you have some projects written in a dynamically typed language where probably 30%+ of bugs would have been caught by static typing and they end up needing to write the equivalent amount of comments to document what they're trying to do. >>39112 The imperative paradigm starts to make more sense when you realize the computer itself is stateful. We should be writing code so that it can be easily worked on and maintained. The moment you start to unnecessarily include currying, have an ideological opposition to state, etc. I think you have the wrong priorities. I will say though FP is closer to the ideal than imperative. Its much easier to test and reason about a pure function. There is a trend away from inheritance heavy OOP particularly because a lot of work surrounds REST APIs.

>>38356 Have you tried Haskell, Agda or F* languages?

>>42167 Not OP (if you're asking him specifically), but doing nontrivial proofs in F* is very painful compared to Coq. Sure, it's nice when z3 does its magic successfully, but when automated proof fails, you have no clue what went wrong. You can use tactics and try to see the intermediate states of the proof, but the experience is worse. Some caveats: I haven't used a ton of automation in Coq either, perhaps it's just a personal distaste. I enjoyed the 1st book of Software Foundations (which uses auto very sparingly), while CPDT (which encourages using automation a lot, IIRC Chlipala even says things like "you should write your own domain-specific automation tactics") was not so easy, and I dropped it after chapter 5. Well, maybe it's just a more advanced book with fewer exercises. Also, I don't have a lot of experience with extracting executable code from a dependently typed language or even just using a dependently typed language to do any kind of nontrivial work (i.e., not exercises). Several months back I made an attempt to formalize some stuff from "Practical Foundations for Programming Languages" by Harper, but I had trouble with his "abstract binding trees" (just ASTs with variable bindings inside - requiring HOAS or de Bruijn indices/levels or just fiddling with substitutions). Hopefully this summer, I'll have some free time to play with it.

Can anyone here explain what dependent typing is and how it works? Most of the explanations I've seen of dependent typing seem to assume that you have a strong mathmatical background and understand Haskell-like functional code. But my background is in languages like C and C++, and I'm much more used to thinking of programming in terms of basic arithmetic and low-ish level memory manipulation than I am the kind of abstract higher-level math that people who understand dependent typing are familiar with. So if someone could explain it without getting too abstract, it would be very helpful.

>>42599 Functions map a type to a type like for an example int to int int add_one(int arg); Dependent functions are a generalization of functions where the output type depends on the value of the input. For example function takes an int, and if the int is even it outputs a bool, and if it is odd it outputs a string. C/C++ and Haskell don't support it but it would look something like type out_type(int arg){ if(arg % 2 == 0){ return bool; }else{ return string; } } out_type(arg) test_func(int arg);

>>42601 Interesting. So, if I understand correctly, you have "type functions" that run at compile time and emit more traditional types. Am I right? If so, it kind of reminds me of C++ templates in a weird way. I've heard you can get things like compile-time leak detection out of dependent types, which is insane if true, since what I've seen thus-far seems pretty simple.

>>42143 > But then you realize it didn't have generics for 10 years when it had generics for maps. (why?) Probably because they were well-informed and had good reasons to leave them out.

>>42719 The C++ approach is really just a shorthand for what programmers do in languages without generics, which is to recreate the same data structures and functions for different types. "Code bloat" implies that the added code isn't doing anything, which is untrue.

>>42607 The type functions can also output other type functions, pretty much anything. There isn't any distinction between type function and regular functions. For example you can have the memory attached to the type and using some extensions like linear types have the type system enforce freeing of all allocated memory at compile time. Another example the length of an array can be part of a type, and an "append" function can return a new array with the length plus one, so you would know the length of vectors at compile time. There are a bunch of different type theores, but the "vanilla" one is Martin-Löf dependent type theory. They can serve as an alternate formal system for mathematics, in comparison to ZF set theory. Most implementation just use them for theorem proving like Agda, Lean, and Rocq. to be honest as far as I know there aren't any compiled languages that use type theory to its full potential, but I'm working on one. https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory https://hott.github.io/book/hott-online.pdf.html

>>42719 That is bullshit, sir. Compile time overhead for generics is insignificant compared to the runtime cost of dynamic dispatch.

>>42804 It has it's cost, not only compile time, but, executable bloat and some cpu cache inefficiencies. But it's still a better choice for many apps. For some apps, boxing/unboxing is not important at all and having fast compile times is a big win. For some apps, dynamic everything is so important that any kind of performance hit doesn't justify using other stack.