tag:blogger.com,1999:blog-178174920347765771.post5671321100639097484..comments2023-10-30T09:20:21.742-07:00Comments on One Div Zero: Types à la ChartJames Iryhttp://www.blogger.com/profile/02835376424060382389noreply@blogger.comBlogger19125tag:blogger.com,1999:blog-178174920347765771.post-66518069429677518202011-08-05T21:10:44.256-07:002011-08-05T21:10:44.256-07:00Higher kinds in Standard ML (SML).
Modular Type C...Higher kinds in Standard ML (SML).<br /><br /><a href="http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf" rel="nofollow">Modular Type Classes</a>, Dreyer, Harper, Chakravarty, section 2.1 Classes are signatures, instances are modulesShelby Moore IIIhttp://copute.comnoreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-34993814775708337152011-07-23T23:18:04.017-07:002011-07-23T23:18:04.017-07:00Higher-kind inference in Haskell.<a href="http://www.haskell.org/onlinereport/decls.html#sect4.6" rel="nofollow">Higher-kind inference in Haskell</a>.Shelby Moore IIIhttp://copute.comnoreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-64164366487746668862010-12-02T03:07:26.956-08:002010-12-02T03:07:26.956-08:00Your chart showed up on programmers.stackexchange....Your chart showed up on programmers.stackexchange.com. I pointed out "I think C# is not well positioned. C# allows and promotes safer programming styles. It should not be measured by the worst thing it allows." C# should go exactly about where Java is (it's type system is slightly richer and that's about it). There are Java -> native code compilers, so one could easily ammendback2doshttp://back2dos.wordpress.com/noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-38028449818595472172010-06-17T22:48:41.125-07:002010-06-17T22:48:41.125-07:00Interesting article, but what the definition of a ...Interesting article, but what the definition of a type?Unknownhttps://www.blogger.com/profile/02263225970855144543noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-74821829322332210022010-06-16T13:33:49.667-07:002010-06-16T13:33:49.667-07:00asflierl,
I think a lot of people have thought th...asflierl,<br /><br />I think a lot of people have thought that. I don't necessarily agree, though. When I'm hacking C I sometimes seriously miss parametric polymorphism.<br /><br />Andreas,<br /><br />Thanks for the info on LF/Twelf. It's a clear example of why my horizontal axis is an oversimplification. I think it would be very interesting to have a proper lambda cube plus one James Iryhttps://www.blogger.com/profile/02835376424060382389noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-5261451860301799362010-06-16T12:19:57.922-07:002010-06-16T12:19:57.922-07:00James,
some remarks:
It's correct that SML&#...James,<br /><br />some remarks:<br /><br />It's correct that SML's first-order modules give you rank-2 polymorphism only. Higher ranks require higher-order modules as e.g. in Ocaml.<br /><br />Haskell 98 has higher kinds. There is no explicit syntax for them, but kind inference figures them out (and there are some tricks to force specific kinds). Moreover, polymorphic abstraction can Andreas Rossbergnoreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-36848466960198327862010-06-16T10:53:43.212-07:002010-06-16T10:53:43.212-07:00So, would you say that on the right side, a langua...So, would you say that on the right side, a language should be on the upper half for the cost of the sophistication to be worth it because of enough safety? And that the lower right corner is deep red because huge sophistication/complexity buys no safety at all?asflierlhttps://www.blogger.com/profile/06454355877884089805noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-77896925241688576052010-06-16T10:32:12.027-07:002010-06-16T10:32:12.027-07:00"hurdle", not "hurtle", i thin..."hurdle", not "hurtle", i think? :-)Raoul Dukehttps://www.blogger.com/profile/07354740962526930549noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-86757591397514034142010-05-15T10:20:45.147-07:002010-05-15T10:20:45.147-07:00Thanks James! Replying only to your first point a...Thanks James! Replying only to your first point about conceptual hurdles:<br /><br />At the limit this it is true that to fully understand sophisticated type logics one has to learn a lot of new skills and ideas. Also it is true that to program with immutable entities requires new skills. <br /><br />However I think this can easily be over-emphasized. Clojure for example has generated a lot jedhttps://www.blogger.com/profile/11258416181053973027noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-60296548173810377112010-05-15T09:36:28.359-07:002010-05-15T09:36:28.359-07:00Jed,
As you move to the right the type logic beco...Jed,<br /><br />As you move to the right the type logic becomes very sophisticated and requires a programmer to think more and more at the meta-level of the type system. There's a real conceptual learning hurtle there. In the lower left area type = representation. That's especially true in language communities where the word "type" means "class" or perhaps "James Iryhttps://www.blogger.com/profile/02835376424060382389noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-16474587608171300612010-05-15T08:52:06.578-07:002010-05-15T08:52:06.578-07:00Given that the pure & total languages have typ...Given that the pure & total languages have type systems that keep them from expressing their own semantics, does it really make sense to say those type systems are "more powerful" than systems that can be used to express their own semantics?<br /><br />To ask this another way, obviously dependent typing is more expressive than just "higher kinded" etc. So that dimension jedhttps://www.blogger.com/profile/11258416181053973027noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-11144556437677432862010-05-15T08:37:46.884-07:002010-05-15T08:37:46.884-07:00One reason this chart is helpful is that we can dr...One reason this chart is helpful is that we can draw a reasonably clear line between languages that are often used to do "real work" and those that typically are not. <br /><br />The line moves over time; mostly up, but somewhat to the right. I'd say it doesn't currently encompass GHC Haskell but people keep trying to pull the line past that point. <br /><br />The incentives jedhttps://www.blogger.com/profile/11258416181053973027noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-14533745863263134682010-05-10T07:58:15.770-07:002010-05-10T07:58:15.770-07:00Jon/Flying Frog,
I did put SML a bit to the right...Jon/Flying Frog,<br /><br />I did put SML a bit to the right of HM because it has a few things that are strictly more powerful than HM. But it's my understanding that SML, even with functors, can't express rank-n polymorphism. If it can then it should definitely move right.<br /><br />I don't know enough about OCaml and F# to know where to place them with certainty.<br /><br />As James Iryhttps://www.blogger.com/profile/02835376424060382389noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-79690226988357253922010-05-09T18:12:38.096-07:002010-05-09T18:12:38.096-07:00My understanding was that, by virtue of kinds, Has...My understanding was that, by virtue of kinds, Haskell '98 had a type system that would be right of second order. In lambda cube speak, second order is terms depending on types, which gives you roughly system F, but that types depending on types, ie kinds, is considered a separate edge in the cube. <br /><br />I'd really like to have all of these things right in my mind, so any Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-56477152890512981012010-05-08T19:04:32.467-07:002010-05-08T19:04:32.467-07:00Nice but what about higher-order module systems?
...Nice but what about higher-order module systems?<br /><br />Maybe you should replace your SML with ML or F# and put SML and OCaml further to the right?<br /><br />Can Java express any static type that OCaml cannot?<br /><br />Should OCaml be at the bottom because it has the Obj module?Jon Harrophttps://www.blogger.com/profile/11059316496121100950noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-69910445884042968052010-05-05T15:16:58.867-07:002010-05-05T15:16:58.867-07:00There should be place for F# somewhere :)There should be place for F# somewhere :)Petrhttps://www.blogger.com/profile/10192613820920972750noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-69956187571229412272010-05-05T14:23:10.527-07:002010-05-05T14:23:10.527-07:00Cool, this is some kind of lambda square, for prac...Cool, this is some kind of lambda square, for practical purposes. <br />Great article; thanks! The diagram will probably grow with more languages being added (from Basic to Coq). <br /><br />(a nitpick: JavaScript's official name is with capital 'S', afaik)Vlad Patryshevhttps://www.blogger.com/profile/13466586996802181998noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-20821656148230563212010-05-05T09:55:50.641-07:002010-05-05T09:55:50.641-07:00Toby, no, total languages are not Turing complete ...Toby, no, total languages are not Turing complete - you can't write an interpreter for Agda in Agda.James Iryhttps://www.blogger.com/profile/02835376424060382389noreply@blogger.comtag:blogger.com,1999:blog-178174920347765771.post-33550122137177417132010-05-05T09:33:24.778-07:002010-05-05T09:33:24.778-07:00Great analysis, I learned a lot reading this!
One...Great analysis, I learned a lot reading this!<br /><br />One small point of clarification - if a language is "pure & total", then can it still be considered Turing complete since the halting problem can be solved on such a language?Tobyhttps://www.blogger.com/profile/06628144829662276775noreply@blogger.com