121–130 of 171 posts
Nice article about type theory. > Why there’s so much research around types if perfectly applying them to programming languages is impractical? Somehow Haskell does this perfectly. Whaddya say to that?
I say, citation needed. Who said "Haskell does it perfectly"? Not to mention the mental overhead of Haskell (which is also not optimal).
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?
What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list ” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)
Now, you may say “okay, the original program doesn't exist anymore, but my language implementation is a term rewriting engine, so I have a current program that I can submit to the type checker”. Alas, most type checkers, Hindley-Milner included, operate on self-contained program fragments (i.e., not containing unbound variables), so you can't just submit any arbitrary program fragment. And, if you didn't want to type-check your original program, how likely is it that you will want to type-check the entire syntactic representation of the current program state?
Earlier quoted context omitted.
Actually, there's one type.
If you're going to shove the system into a typed model, then sure there is one type. But then you've kind of missed the point...
You literally have to count the types by analyzing the grammar. So for the lambda calculus, you have lambda=1, halt. So does a single type mean no types or literally one type?
What's the advantage of thinking that 1 type actually equals 0 types? I don't see any, so in my mind, all languages are unityped or have a richer type structure. Whether a richer type structure is desirable is a separate question.
Earlier quoted context omitted.
What do you consider basic? Algorithm W for ML type inference is pretty basic, but powerful too. Or are you looking for something even more expressive?
What I meant by basic was the description of types provided by a language - usually in an introductory text you might read when learning a new language. I probably didn't articulate that correctly. But I guess what I was referring to as a "middle ground"qa any resources for learning about types systems written in a similar approachable tone like this article. This was another article I read recently that I thought wa…
https://mitpress.mit.edu/books/types-and-programming-languag...
You can find some earlier PDF drafts online if you Google.
mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?
> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions. mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?
My reading is that it was invented by Scotus as Haecceity ! This was required by Catholic Christianity because of the difficulty that The Creed introduces about the identity of God - there are three entities which represent God, the Trinity - how to account for this? Well; the thisness of God is joined with the thisness of man, the thisness of the creator and the thisness of the thing which is motion (I have never understood The Holy Spirit). You can think of this as multiple inheritance! Theologians then had to account for "why three" as you can carry on making aspects of god with this mechanism infinitely, god the mother, god the lover, god the hunter and so on. But there are three - why? The answer was provided by Scotus's student Occam, entities should not multiply beyond necessity and hence there are three aspects of god because it is necessary for creation that there are.
The fun bit it that this procession of thought is somewhat guessed at because writing things like this down or debating them publically was a quick route to the afterlife via a bonfire!
Earlier quoted context omitted.
I find that a significant fraction of the bugs introduced to the code bases I've worked on that have dynamic typing are due to issues that even a rudimentary static typing system would prevent at compile time. I'm struggling to grok how a language with no type system might look. Something post-modern and Picasso-esque? To use data in a meaningful way in a program it must be possible to reason about it, and that requi…
Assembly languages are untyped. Nothing prevents you from reinterpreting a memory address as a type it is not. (Except possibly alignment issues.)
What a great piece! I wish the author would expand on this piece with either more installments or a even short book. I find myself interested in type systems as it relates to programming language design but I haven't found much middle ground between the basic types described in introductory texts about a language and the opposite extreme heavy academic texts such as the ones the author is breaking down in this articl…