Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Where Do Type Systems Come From?

blog.felipe.rs

Post reply on HN
Print view View original

141–150 of 171 posts

Re: Where Do Type Systems Come From?

#141

Post by leshow »

evincarofautumn wrote: post #88
didibus wrote: post #82

Earlier quoted context omitted.

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. This happens quite often. Take datastructures. It is often very useful to structure different types of data together in a common structure. Now in most cases, you don't know in advance which type will go where in the datastructure, as the data might only be known or derived at runtime. In fac…

It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic typ…

Can you explain what you mean by comparing universal and existential quantification to dynamic languages? Existential quantification is often used in statically typed languages and can be valuable in some cases (no pun intended). In Rust, for instance, you can say fn f() -> impl Fn(u8) -> u8 or something similar. This is existential quantification, because you're saying that f returns a type that is some Fn(u8) -> u8. This can expressiveness can be powerful in a type system. I don't see how it relates to dynamic languages.

Re: Where Do Type Systems Come From?

#142

Post by leshow »

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

What languages have you tried? I think once you experience a language with types outside of the run of the mill Java/C#, you will get more excited about it. Ocaml, Rust, Haskell, Purescript, etc. Haskell for me was the one that got me excited about types.

Re: Where Do Type Systems Come From?

#143

Post by leshow »

ridiculous_fish wrote: post #8
smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

> I get that these underpin the technology we as programmers use every single day Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?

C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.

Re: Where Do Type Systems Come From?

#144

Post by leshow »

jholman wrote: post #91
AnimalMuppet wrote: post #10

Earlier quoted context omitted.

If. I suspect that smcl can't get excited about type systems because of not seeing the benefit. For me, types are sets of possible values, plus sets of valid operations on those values. I don't much care where they come from. As far as I am concerned, they are an engineering construct to make programming easier and safer, and are interesting only to the degree that they accomplish those goals. Any connection to pure…

Yes, precisely. I'm very interested in theory (by the standards of non-academics). I'm very interested in pragmatic type systems. I've spent a few hundred hours on trying to learn type theory, in the mathematical sense. The only thing I have personally found useful, so far, in type theory, is the notion of sum types and product types. But that's just jargon for things I was able to deduce from a shallow study of many…

I don't think approaching type systems from the mathematical angle is much help either. When I was learning Haskell, I started to try to learn category theory to develop a better understanding of what was going on. In the end I decided my time was better spent learning Haskell, and not category theory. Where they share words I look shallowly into the mathematical concept, but the understanding I develop is how it relates to me in a programming context. That doesn't mean I don't value that there is a mathematical basis for it though.

Re: Where Do Type Systems Come From?

#145

Post by catnaroek »

johncolanduoni wrote: post #131
catnaroek wrote: post #90

Earlier quoted context omitted.

You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?

Why is that required? There's nothing stopping you from only giving the list a precise type after an element has been added. This mirrors the way statically typed languages with inference handle the same situation (except they wait for evidence that it's being used as a list of Ts, instead of the actual act).

> Why is that required?

Say, because you want to use that reference cell in two different threads.

Re: Where Do Type Systems Come From?

#146

Post by z3t4 »

heavenlyblue wrote: post #114
gizmo686 wrote: post #66

Earlier quoted context omitted.

Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can…

"f(x) + g(x)" This example is way too trivial to explain why type systems are generally undecidable. Let's imagine: def f/g(x): if isinstance(x, str): return 6 elif isinstance(x, int): return 'a' It is decidable for any type of x that is previously known. More importantly, type systems were essentially created to be able to prove whether a given expression is decidable or not. x = 1 print_int(x) x="a" print_string(x)…

the real world is not strictly typed, i think types are for the compiler rather then humans. Im however a big fan of runtime bound checking so that the program always have a sane state.

Re: Where Do Type Systems Come From?

#147

Post by kazinator »

igravious wrote: post #107
kazinator wrote: post #26

Earlier quoted context omitted.

Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)

ba-dum tss! are you here all week?

Sure---if catering keeps that sirloin roast coming for another seven days. Have you tried it?

Re: Where Do Type Systems Come From?

#148

Post by z3t4 »

leshow wrote: post #142
smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

What languages have you tried? I think once you experience a language with types outside of the run of the mill Java/C#, you will get more excited about it. Ocaml, Rust, Haskell, Purescript, etc. Haskell for me was the one that got me excited about types.

ive only used vbscript and javascript extensibly. when ive tried java and #C ive been annoyed by the verbosity of types. and when looking at haskel or ocaml im just confused. for me types are an optimization or extra documentation for undescriptive naming, like str x, int y, list z. vs. name,age,friends. so i want to know what im missing, will there be less bugs and regressions? will i be more productive ?

Re: Where Do Type Systems Come From?

#149

Post by z3t4 »

Jtsummers wrote: post #27
zzzcpan wrote: post #13

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with…

What are the other approaches for preventing bugs you have in mind that are novel or increasing in application? We've done testing since the start. Still many bugs. We've done ad hoc modeling (behavior driven) for years with some improvement. Formal methods aren't popular but are successful at least at some (small to the low end of medium) scales or within portions of large scale systems. Type systems can and have be…

what ive found most effective at finding bugs is to have two systems, the data represented in two different type systems, then cross check them on crucial intervals. the second most effective at finding bugs is to check function parameters both when entering the function and when returning from the function, for bound, range, etc. and third... study and understand the code, actually writing code that is easy to coprehend. then tests are very good at preventing regressions. despite this, there will still be bugs though smile so debuability, effective debugging is really important!

Re: Where Do Type Systems Come From?

#150

Post by naasking »

alexashka wrote: post #135
naasking wrote: post #125

Earlier quoted context omitted.

Types and Programming Languages is the go to book, and it's very accessible despite being a textbook: https://mitpress.mit.edu/books/types-and-programming-languag... You can find some earlier PDF drafts online if you Google.

I have the book and I must warn people, it is not THAT accessible - this is not evening reading for an hour, this is work.

You'll have to define accessible then. Learning anything takes work.
Post reply on HN