tag:blogger.com,1999:blog-7486674684844560197.post8348221328032435879..comments2013-02-22T06:53:13.919-08:00Comments on The Paralyzing Paradoxes of Professor Polaro: The Logical Basis of Evaluation Order and Pattern-MatchingNoamhttp://www.blogger.com/profile/09175792123472366590noreply@blogger.comBlogger4125tag:blogger.com,1999:blog-7486674684844560197.post-7416893972980999372009-05-23T14:48:46.725-07:002009-05-23T14:48:46.725-07:00thanks A. and pingouin for the well wishes. Pal-K...thanks A. and pingouin for the well wishes. Pal-Kristian, yes, that's the ultimate question, and I think I'd have to do a lot more hacking before I could come up with good answers. But I have some ideas. The most basic (that comes directly from polarized logic) is just that a language should allow programmers to define both positive and negative types, by describing their constructors or destructors. And that pattern-matching should be available not only for eliminating positive types (as usual in ML/Haskell), but also for introducing negative types. The latter can also be seen as typed control operators -- in my thesis I only describe undelimited control, but I believe the approach extends pretty nicely to delimited control operators, which seem to be of more practical value.<br /><br />There's a lot of other areas in type theory where I think polarity and focusing can be useful concepts for simplifying and extending existing approaches, particularly to better account for effects and equality. My thesis works through the theory of refinement types. I think there is something to be said about dependent types and type abstraction as well.Noamhttps://www.blogger.com/profile/09175792123472366590noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-7881881340169464742009-05-21T10:26:39.353-07:002009-05-21T10:26:39.353-07:00Great Thesis!
One question: Given your insights ...Great Thesis! <br /><br />One question: Given your insights into polarized logic, if you had to create a practical language - what would it look like, and what features would it have that doesn't exist in ML/Haskell or languages based on CBPV?Anonymoushttps://www.blogger.com/profile/11706415958770692001noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-51515408101109640512009-05-11T02:56:00.000-07:002009-05-11T02:56:00.000-07:00Bravo docteur.Bravo docteur.mrpingouinhttps://www.blogger.com/profile/12886021564678353584noreply@blogger.comtag:blogger.com,1999:blog-7486674684844560197.post-64293476261598862902009-05-08T12:48:00.000-07:002009-05-08T12:48:00.000-07:00Congratulations, and happy post-doc in Paris/PPS! ...Congratulations, and happy post-doc in Paris/PPS! Pierre-Louis Curien spoke highly of your work during a proof theory course.A.https://www.blogger.com/profile/03954463506974679294noreply@blogger.com