User loginNavigation |
LtU ForumTeaching challenge: culturally enriching formulae-as-typesIn a G+ request, Norman Ramsey says he wants spice up his PL survey course with a little bit of "cultural enrichment" to show my students the "propositions as types" approach to proof. He's looking for source materials, and, I take it, experiences from people who have tried to teach similar things. Active Variables in Common LispA feature I lifted from ksh93, I thought I would share with LTU. Active variables in Common Lisp; variables with callbacks on reading and writing. Possibly a useful feature that I rarely see in modern programming languages. Peak AbstractionToday I learned a new term from a blog post:
The complete blog post rags mostly on perf issues, but I'm more interested in the complexity implications. I felt myself go through this before, and to be honest the more powerful the language, the worse my peak abstraction got. It was only when moving to a less expressive language (C# rather than Scala) that I had incentive to keep it simple. Has anyone else found themselves in an abstraction trap and come down as they grew as a programmer? What can we do in PL design to avoid, or at least discourage, overuse of abstraction? Is this a case of where less might be more? Evolution of mainstream programming language paradigmsI have been thinking recently about what makes the mainstream language a mainstream. And I think that the mainstream programming language paradigms generally evolve using the following evolution pattern:
In paradigm for mainsteam languages we could obviously see the chain when the following level organizes the previous one.
As we see here, the next generation always abstracted previous level, and it was exactly one level abstraction. The functional languages so far do not fit into this picture. The LISP was not one step jump, they are many step jump. Many features of LISP got into mainstream (the latest were garbage collection and lambda expressions), but there are some things to integerate (like internal DSLs). So LIPS was a kind of peak experience for programming language paradigms. To me Haskell and ML did not offer appropriate one-step abstraction over structured programming. ML modules were only half-step abstraction over data and procedures, since data and functions were still different concepts. There were also halfway abstraction of data and behavior in the form of lambda expressions, but it was a single-method object, but GUI toolkits (current complexity challlenge at that time) required many-methods objects for appropriate abstraction. If we look to the sequence, the next step should be some abstraction over components, and I think it would be component systems. We could see the early component systems as libraries now (Spring, GUI toolkits, EJB3, Plugins in Eclipse and IDEA, UML2, etc). I have written more details why I think so in this document. It also contains an initial list of requirements for the possible next generation mainstream language. I think it will be a component system programming langauge (CSPL). So the document is named CSPL Challenge. I think typing and and type-checking component systems would be a quite interesting research topic. And maybe there are already some results out there, that fit requirement exactly. Syntax Desugaring Algorithm QuestionHello all! I'm building a lisp in F# using FParsec. The language is called AML. I have a reader and an interpreter running, and I just now built a 'desugaring' function to rewrite AML code. For example, the expression a.b desugars to (access :m:b a). This is all well and good, but there is a problem. Once the desugarer outputs the transformed code text, it will be passed to the reader. As mentioned, the reader uses FParsec to create the AST. When FParsec encounters an unparsable character sequence, it propagates some nice error position information, a somewhat useful error message, and a description of the where the code text cannot be parsed. The issue is that this information will not be very meaningful to the user once the reader gets its input from the desugarer rather than the original user's code. How do interpreters typically preserve this error information across transformed code so that the user can get error messages in terms of his original code? Any practical or research material is nice. For run-time performance and implement-ability, I prefer a simple algorithm to a more sophisticated one. In truth, I am a language development newbie in many respects. Thank you greatly! LastCalc: A web-based REPL for a pure functional programming language with a flexible syntax and parserLastCalc is a very experimental web-based tool that started out as a kind of Google Calculator but with a "REPL"-style user interface that permits variable assignment. Like Google Calculator it supports basic math, and conversions between different measurement types like miles or kilograms (relying on the Java JScience library for this functionality), all with a relatively natural language syntax. Along the way we added the ability to define parameterized functions, and then pattern matching on datastructures like lists and maps (inspired by ML), including recursively defined functions, all in a friendly AJAX-based web user interface. LastCalc's parser is extremely robust, doing a reasonably efficient best-first search with backtracking to interpret its input. Anything it can't interpret is ignored. Soon people will be able to share the parameterized functions they've designed, ultimately allowing people to collaboratively "teach" LastCalc how to interpret things that it currently cannot. The link above provides a quick walk through of the system along with a link to it so that you can try it for yourself. Language outline of Modern Eiffel (SW Verification)Link to the original blog entry. In the course of this blog I am going to use a variant of Eiffel called Modern Eiffel is an object oriented language. All types are defined by
class
MY_CLASS -- class name
create
creator1(a:A) ...
creator2 ...
feature
some_function(b:B): RT ...
some_command(c:C) ...
all(i:INT) some_property(i)
proof
...
end
CHAR = CHARACTER -- type alias
invariant
... -- consistency conditions
end
Comments begin with "--" and span to the end of the line. There are some basic types. These are types with built-in functions and
immutable class
BOOLEAN
feature
implication alias "=>" (o:BOOLEAN): BOOLEAN
external "built_in" end
negated alias "not": BOOLEAN
external "built_in" end
conjuncted alias "and" (o:BOOLEAN): BOOLEAN
external "built_in" end
disjuncted alias "or" (o:BOOLEAN): BOOLEAN
external "built_in" end
...
end
Functions can have operator aliases for unary and binary operators. I.e. not a -- highest precedence a and b a or b a => b -- lowest precedence
have the expected meaning. The most important boolean operator is the A class can inherit features from other classes. For this blog entry
class
T
inherit
-> ANY
COMPARABLE
...
end
The symbol "->" stands for conforming inheritance. For the following
class
COMPARABLE
feature
is_equal(o:like Current): BOOLEAN
external "built_in"
ensure
all(x:like Current) x=x
all(x,y: like Current) x=y => y=x
all(x,y,z: like Current) x=y => y=z => x=z
-- "=" has higher precedence than "=>"
end
end
The feature "is_equal" is used in Modern Eiffel to define equality. It x=y => y=z => x=z Usually one would expect the transitivity law written as x=y and y=z => x=z
Both forms are equivalent. This will be proved later. If possible we Each class inheriting from COMPARABLE can redefine (i.e. overwrite) the People with experience in imperative languages like C++, C#, Java, etc. Inductive data types are best explained with some examples. The simplest
case class
COLOR
create
red
green
blue
end
The keyword "case" introduces an inductive class. The class COLOR has
r: COLOR := red
g: COLOR := green
...
The assigment operator ":=" can be used to initialize variables. In a similar fashion we can define a class WEEKDAY
case class
WEEKDAY
create
monday
thuesday
wednesday
...
sunday
feature
next: WEEKDAY
...
end
The class WEEKDAY has a feature "next" in order to calculate the next
next: WEEKDAY =
inspect Current
case monday then thuesday
case thuesday then wednesday
...
case sunday then monday
end
Inductive types allow case expression to make distinctions on how the The above form is the short form of a function definition. The function
next: WEEKDAY
require
... -- precondition(s)
ensure
Result =
inspect Current
case monday then thuesday
...
end
end
The keyword "Result" indicates the return value of the function. The Objects of the very simple inductive types like COLOR and WEEKDAY just Let us consider the following class
case class
OPTIONAL[G]
create
none
value(value: G)
end
This class is generic. A generic class is a type constructor. It can The class has just two creators: "none" and "value". The object n: OPTIONAL[INT] := none has no value and the object i7: OPTIONAL[INT] := value(7)
has the value 7. The name "value" is used for the creator and for an The access of the attribute "value" is illegal, if the corresponding In order to introduce pattern matching we use a contrived example of a
value_plus_100(o:OPTIONAL[INT]) =
inspect o
case none then -1
case value(i) then i+100
end
The function "value_plus_100 is contrived, because one would not write The first case clause is for objects created with the "none" creator. The second case clause is for objects which have been created with the The function "value_plus_100" can be written in a form which accesses
value_plus_100(o:OPTIONAL[INT]) =
inspect o
case none then -1
case value(_) then o.value + 100
end
The wild card "_" is used to supress the creations of a fresh local The full expressive power of inductive types unfolds with recursively
case class
UNARY_NATURAL
create
zero
succ(pred: UNARY_NATURAL)
feature
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = ...
times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL = ...
power alias "^" (o:UNARY_NATURAL): UNARY_NATURAL = ...
...
end
The class UNARY_NATURAL is highly inefficient to do arithmetics. But it The class UNARY_NATURAL has tow creators. One to create the number 0 and The recursive structure of the type can be used to define the functions
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL =
inspect Current
case zero then o
case succ(p) then succ(p+o)
end
times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL =
inspect Current
case zero then zero
case succ(p) then o + p*o
end
power alias "^" (o:UNARY_NATURAL): UNARY_NATURAL =
inspect o
case zero then succ(zero)
case succ(p) then Current * Current^p
end
Recursive functions for inductive types defined in this fashion have the case succ(p) then succ(p+o)
This branch is entered only if the current object has been created with succ(p+o)
uses the predecessor to make the recursive call "p+o", i.e. it calls the Another classic inductive type is defined by the class LIST.
case class
LIST[G]
create
nil
cons alias "::" (first:G; tail:LIST[G])
feature
...
end
A list is either empty or is an element (the first element) followed by If a creator has two arguments, a binary operator can be used as an lst: LIST[INT] := 1::2::3::nil -- parsed as 1::(2::(3::nil)) -- equivalent to cons(1,cons(2,(cons(3,nil)))
Since lists are very expressive on its own and can serve as models an This blog has introduced some basic language elements of Modern Eiffel. Keep in mind that all sorts of mutable structures and imperative STEPS 2011 Progress Report (personal computing in 20kLOC)
The recent mention of the Nile programming language reminded me to post about the STEPS 2011 Progress Report.
The overall goal of STEPS is to make a working model of as much personal computing phenomena and user experience as possible in a very small number of lines of code (and using only our code). Our total lines of code‑count target for the entire system “from end‑user down to the metal” is 20,000, which—if we can do a lot within this limit—we think will be a very useful model and substantiate one part of our thesis: that systems which use millions to hundreds of millions of lines of code to do comparable things are much larger than they need to be.... Our general approach is to pick an area whose parts seem to be related—for example: 2.5D anti‑aliased alphaed computer graphics—try to find the mathematical relations that cover the desired phenomena, design a “problem oriented language” (POL) that is a “runnable math” version of the mathematics, implement that language, then use it to write the program code for the target area.... STEPS is now to the point where it is more fun to use and demonstrate than to talk and write about. Quite a bit of the original proposal is now working well enough to give all our presentations and write this entire report for the NSF and Viewpoints Research Institute websites. In the STEPS system, this document is live: the examples are actually runnable demos; the code shown is changeable and testable, etc.Previous discussion of this project on LtU includes:
Non-deterministic versus parallel function applicationGreetings, Ehrhard and Regnier described a functional programming language -- the differential lambda calculus -- which added to the lambda calculus a commutative monoid structure and a differential operation. One feature of this calculus is that application is linear in the first argument. I am studying a weaker system that adds only the commutative monoid structure, and I insist that application preserves addition in the first argument (which is implied in E.R.'s system). This means: The above has the feel of non-determinism to it. Given 'g' or 'h' applied to 'm' the result is 'g' applied to 'm' or 'h' applied to 'm.' However, in general: So it is not as if 'g' makes a non-deterministic choice of 'm' or 'n.' While some have called this non-determinism, others have called parallelism. Any thoughts on what the correct word describing such an application might be? By jdgallag at 2012-01-24 18:46 | LtU Forum | login or register to post comments | other blogs | 431 reads
Visual Studio AchievementsFrom the it-had-to-happen department, Announcing Visual Studio Achievements Beta:
What's troubling is that the list of achievements in fact includes various anti-achievements such as Go To Hell (for using In the grim future of gamified PLT, you'll not only be tyrannised by your BDFL, your aberrances from the One Microsoft Way will be broadcast to your peers in realtime. Also: XCode achievements on Twitter. |
Browse archivesActive forum topics |