141–150 of 198 posts
I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)
Earlier quoted context omitted.
Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. I have never met a daily user of these tools that find this to be the bottleneck. In practice yo…
> Type inference isn't important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. What I'm saying is that I don't like this direction, because type inference is very important to me. > Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure.…
On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does, I figure some default type systems could be created for a specific style of Shen and/or specific libraries. Or something similar done in a ML.
http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
Earlier quoted context omitted.
No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the…
> No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using fi…
Haskell programmers also use higher order logic, which is also common now in Java and C#.
Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no e…
> Proving F matches the type is arbitrary hard and is impossible to automated in general So what? Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...
Mainstream languages will gain much more from better iterators than by a ton of effort that just proves your indexes are within bounds.
> A type is a collection of possible values Ok, but do two collections with the same values always correspond to the same type?
Earlier quoted context omitted.
> No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using fi…
I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
Earlier quoted context omitted.
> Type inference isn't important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. What I'm saying is that I don't like this direction, because type inference is very important to me. > Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure.…
I like your proposal of first-order, dependent types. Shocked I havent heard of it before now given advantages. I hope someone helps you build it. On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does…
IMO, the topmost priority in a type system designed for programmers ought to be automation, not expressiveness. Programmers don't spend their time proving deep theorems. Most of what a programmer does is actually fairly boring, but it ought to be done correctly, reliably and within a reasonable time frame.
Earlier quoted context omitted.
I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
> Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.
Earlier quoted context omitted.
> Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
Hmm, I don't think you're being very charitable. That these programmers can write working programs suggest they sufficiently understand disjunction, conjunction, negation, conditionals and quantification. Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.
Earlier quoted context omitted.
Is it set-theoretic though? The article states: > A type is a collection of possible values. "Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? Would you also complain if a Web page giving an informal introduction to topology said "a space is a collection of points"? Keep in mind that in HoTT, types are spaces and points are values, and hence those tw…
> "Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? I think it's still wrong, but let's get concrete in the more unusual type systems to check. What is the "collection of values" for a type in TyPiCal [1]? What is the "collection of values" for substructural types, like linear types [2] or affine types [3]? I don't think "collection", set-based or ot…