User loginNavigation |
AdminLtU is now running in a new, more stable environmentLtU has experienced a long period of downtime recently. Its software infrastructure was outdated enough that it became difficult to maintain when problems arose. It has now been migrated to a brand new environment. It should be much more stable from now on. CaptchaNote to those who tried to sign up but couldn't get passed the broken captcha: we removed it, so please try again. Email me directly to activate the account, once you've created it and got the automatic email. Copattern matching and first-class observations in OCaml, with a macroCopattern matching and first-class observations in OCaml, with a macro, by Paul Laforgue and Yann Regis-Gianas:
Codata isn't well supported enough in languages IMO, and supporting it via a simple macro translation will hopefully make it easier to adopt, at least for any language with GADTs. Happy Birthday, dear Lambda: 17 is good editionSeventeen years ago to the day, LtU was born. I guess it's about time I stop opening these birthday messages by saying how remarkable this longevity is (this being the fate of Hollywood actresses over 25). Still, I cannot resist mentioning that 17 is "good" (טוב) in gematria, which after all is one of the oldest codes there are. It's is very cool that the last couple of weeks had a flurry of activity. This old site still got game. I will not try to summarize or pontificate. The community has grown too big and too unruly for that and I have been more an absent landlord recently than a true participant (transitioning from CS to being a professional philosopher of science and having kids took a bit more of my free time than I expected). One thing I always cherished about LtU was that we welcomed both professional, academic work, and everything and anything that was cool and fun in programming languages. It was never a theory only site. So here's a little birthday party game instead of a long summary. Which new (or old) languages inspire you to think that a good language can smoothly allow people to reach heretofore hard to reach semantic or abstraction levels? I mean things that affect how the little guy thinks, not formal semantics, category theory, or what have you. I'll start with two unconventional languages that I have had the pleasure (and exasperation) of using recently. Both are in some respects descendants of Logo, the language through which I was introduced to programming when I was a ten year old child in Brookline. They are NetLogo and ScratchJr. NetLogo is a language for building agent based models (here's a classic ABM for you to enjoy; if you install NetLogo there's an implementation in the model library). While some aspects of the language semantics (and syntax) are irritating, NetLogo is very good at what it does. I may say more in the comments, but the key is that a simulation consists of multiple agents, who can move and interact, and the language makes building such simulations straightforward. There is a central clock; you can address multiple agents using conditions ("ask guys with [color = red] [die]"); implicitly have code run by each agent etc. In fact, you hardly think about these issues. If you have no previous background in programming, it feels natural that keeping track of these and other details is not part of the task programming. ScratchJr is for young kids. It allows them to create little animated scenes, which may be responsive to touch and so on. You can record sounds and take pictures and use them as first class elements in your animations. But the nice thing for me was to notice how natural it is for kids to use the event-driven model (you can "write" several bits of code, and each will execute when the triggering event happens; no need to think about orchestrating this) as well as intuitively understand how this may involves things happening concurrently. These things just emerge from the way the animations are built, they are not concepts the programmer has to explicitly be aware of (which is a good thing, considering she is typically a five year old). When I see philosophy students writing netlogo and reasoning about the behavior of the agents and when I see kids playing with ScratchJr, I am reminded why I found this business of "engineering abstractions" so enticing when I first used structured programming to design vocabulary for the program I was writing and when I heard some language described as a language for stratified design. So which are your nominations for cool language based abstractions, for the little guy? Just to give us all some motivation and maybe get me worked up enough to finally delve into algebraic effects? Happy birthday, LtU-ers. Keep fighting the good fight! Do Be Do Be DoMonads and algebraic effects are general concepts that give a definition of what a "side-effect" can be: an instance of monad, or an instance of algebraic effect, is a specific realization of a side-effect. While most programming languages provide a fixed family of built-in side-effects, monads or algebraic effects give a structured way to introduce a new notion of effect as a library. A recent avenue of programming language research is how to locally define several realizations of the same effect interface/signature. There may be several valid notions of "state" or "non-determinism" or "probabilistic choice", and different parts of a program may not require the same realization of those -- a typical use-case would be mocking an interaction with the outside world, for example. Can we let users locally define a new interpretation of an effect, or write code that is generic over the specific interpretation? There are several existing approaches, such as monad transformer stacks, free monads interpreters, monad reification and, lately, effect handlers, as proposed in the programming language Eff. Frank, presented in the publication below, is a new language with user-defined effects that makes effect handling a natural part of basic functional programming, instead of a separate, advanced feature. It is a significant advance in language design, simplifying effectful programming. Functions, called operators, do not just start computing a result from the value of their arguments, they interact with the computation of those arguments by having the opportunity to handle any side-effects arising during their evaluation. It feels like a new programming style, a new calling convention that blends call-by-value and effect handling -- Sam Lindley suggested the name call-by-handling. Frank also proposes a new type-and-effect system that corresponds to this new programming style. Operators handle some of the effects raised by their arguments, and silently forward the rest to the computation context; their argument types indicate which effects they handle. In other words, the static information carried by an argument types is the delta/increment between the effects permitted by the ambient computation and the effects of evaluating this argument. Frank calls this an adjustment over the ambient ability. This delta/increment style results in lightweight types for operators that can be used in different contexts (a form of effect polymorphism) without explicit quantification over effect variables. This design takes part in a research conversation on how to make type-and-effect systems usable, which is the major roadblock for their wider adoption -- Koka and Links are also promising in that regard, and had to explore elaborate conventions to elide their polymorphic variables. Another important part of Frank's type-system design is the explicit separation between values that are and computations that do. Theoretical works have long made this distinction (for example with Call-By-Push-Value), but programmers are offered the dichotomy of either having only effectful expressions or expressing all computations as values (Haskell's indirect style). Frank puts that distinction in the hands of the user -- this is different from distinguishing pure from impure computations, as done in F* or WhyML. If you wish to play with the language, a prototype implementation is available.
Do Be Do Be Do
(arXiv)
AdminAs many of you know, the email functionality of the website has not been working for a very, very long time. In addition, all new users are still being approved by me, to combat spam. All this means manual work by me, prompted by frustrated emails by new members. Alas, given other commitments, I find that the backlog is growing and I simply cannot find the time to handle these emails (i.e., approve the user, set an initial password, let them know and ask them to change it). If any member want to help me with this, I would be grateful. This will involve getting extra admin privileges on the site, after which I can forward the requests in the pipe line to you to approve. Thanks! Dynamic Witnesses for Static Type Errors (or, ill-typed programs usually go wrong)Dynamic Witnesses for Static Type Errors (or, ill-typed programs usually go wrong) by Eric L. Seidel, Ranjit Jhala, Westley Weimer:
Sounds like a great idea to make type systems more accessible, particularly for beginners. The current limitations are described the discussion, section 54:
It's also not clear whether this would produce proper witnesses for violations of higher kinded types or other more sophisticated uses of type systems. There are plenty of examples where invariants are encoded in types, eg. lightweight static capabilities. By naasking at 2016-06-18 12:51 | Admin | login or register to post comments | other blogs | 33775 reads
How to Build Static Checking Systems Using Orders of Magnitude Less CodeHow to Build Static Checking Systems Using Orders of Magnitude Less Code, by Fraser Brown Andres Notzli Dawson Engler:
Looks like an interesting approach with some compelling results, and will make a good tool for the toolbox. See also the Reddit thread for further discussion. GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and LazinessGADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness by Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon Peyton Jones:
Another great paper on a very useful incremental improvement on GADTs as found in Haskell, OCaml and Idris. Exhaustiveness checking is critical for a type system's effectiveness, and the redundant matching warnings are a nice bonus. Domain settingsI am about to make some changes to the name server definitions. Since changes take time to propagate, you may have trouble reaching the site for awhile. If this happens, try using the .com domain instead of the preferred .org domain. By Ehud Lamm at 2014-10-04 11:24 | Admin | login or register to post comments | other blogs | 20285 reads
|
Browse archives
Active forum topics |
Recent comments
25 weeks 4 days ago
25 weeks 4 days ago
25 weeks 4 days ago
47 weeks 5 days ago
52 weeks 19 hours ago
1 year 1 week ago
1 year 1 week ago
1 year 4 weeks ago
1 year 8 weeks ago
1 year 8 weeks ago