tag:blogger.com,1999:blog-46144544133801078132024-03-08T17:06:31.193-03:00One Mistake After AnotherDanielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-4614454413380107813.post-25706472614927979812012-05-03T10:00:00.001-03:002012-05-03T10:00:23.538-03:00The Essence of Dynamic TypingDynamic vs Static typing discussions exist probably since Bertrand Russel tried to formalize <a href="http://en.wikipedia.org/wiki/Set_theory">set theory</a> and somebody questioned his <a href="http://c2.com/cgi/wiki?BondageAndDisciplineLanguage">preferences</a>. One presumes, like all other discussions in math and science, it would be mostly resolved by now due to the sheer pressure of evidence and well thought arguments from both sides. Sadly, like most debates in programming this one is filled with misconceptions and both sides are famous for speaking past each other. I'll try to find the essence of dynamic typing, the one feature that is supposed to add expressiveness to dynamic typing (not dynamic languages in general, this won't cover Lisp-like macros, eval, Smalltalk <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">become:</span>, reflection, code-loading, etc.) and see what it fundamentally means.<br />
<br />
Dynamic typing offers us the possibility of writing programs that are partially defined and may fail due to certain inputs. Let's see an example (using Javascript syntax):<br />
<br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> function example(b, x) {</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> if (b) {</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> return length(x);</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> } else {</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> return x * 2;</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> }</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;"> }</span></span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">The function above is well defined if b is true and x is applicable to length() or if x is applicable to *2. The programs </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">example(true, "abcdef")</span><span class="Apple-style-span" style="font-family: inherit;"> and </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">example(false, 3)</span><span class="Apple-style-span" style="font-family: inherit;"> give both the same result and should not fail at runtime, while </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">example(false, "abcdef")</span><span class="Apple-style-span" style="font-family: inherit;">, </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">example(true, 3)</span><span class="Apple-style-span" style="font-family: inherit;">, </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">example(3, false)</span><span class="Apple-style-span" style="font-family: inherit;">, etc., have undefined behavior. The essence of dynamic typing is to move this undefined behavior to run time, instead of trying to disallow it at compile time, allowing more programs to be expressed.</span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
It's also possible to express and try to run an infinite amount of programs that only evaluate to undefined behavior, without hope of useful work being computed. Most, if not all, in the static typing camp find this downside to be greater than the added expressiveness.<br />
<br />
Going back to our example I think it's safe to say that there's no value in the programs exhibiting only undefined behavior (i.e. all paths lead to crashes) and there's value in finding as early as possible if a program goes in that direction. OTOH dynamically typed programs usually have many valuable paths even if there exist undefined paths. Actually the whole dynamic typing argument can be boiled down to:<br />
<blockquote class="tr_bq">
The value of executable paths is greater than the value of unexecutable paths. Undefined behavior in unexecutable paths can not be observed.</blockquote>
In this point of view trying to avoid the execution of paths that a program don't execute is a wasteful tautology: "avoid doing what you won't do" is a meaningless advice.<br />
<br />
Aside, it's interesting to notice that such language can have an erasure model of compilation and don't require runtime tags. Of course it will be unsafe if the unexecutable paths suddenly are executed but this is another issue.<br />
<br />
The example program can also be written in OO style, but the idea is the same.<br />
<br />
Fundamentally dynamic typing relies on undefined behavior for some code paths which, surprisingly, exist in almost all statically typed languages. In Haskell, for example, it's easy to add undefined behavior by using the aptly named <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">undefined</span> value. What dynamically typed languages offer is a single static type (i.e. any or object or stuff) for all expressions so you can write down any kind of expressions and they all type check. One could do the same in Haskell using a modified Prelude and not using <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">data</span> declarations, essentially having something like this:<br />
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><br />
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> data Any = B Bool | N Int | C Any Any | Nil | F (Any -> Any)</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> -- we support booleans, numbers, cons cells, nil and functions</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> length (Nil ) = N 0</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> length (C car cdr) = case (length cdr) of</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> N n -> 1 + n</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> -- let it crash on other paths</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> example (B True) x = length x</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> example (B False) (N n) = N (n * 2)</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">This is the has the same behavior and static guarantees. For this small example the static typing won't get in the way of writing the same programs we would in a dynamically typed language. Of course this breaks down when we want to declare our own data types, because we need to extend </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">Any</span><span class="Apple-style-span" style="font-family: inherit;"> to support structures. We can do it using other features of Haskell or extend the language, but this exercise is pointless. Any Turing-complete language can encode another Turing-complete language and any static type system can express a dynamic type system, because it is statically unityped.</span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">If Haskell had no </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">undefined</span> value (or any equivalent) we could still encode the undefined behavior like this, using <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">U</span> as the undefined value:<br />
<br />
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> data Any = B Bool | N Int | C Any Any | Nil | F (Any -> Any) | U</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><br />
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> length (Nil ) = N 0</span></div>
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> length (C car cdr) = case (length cdr) of</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> N n -> 1 + n</span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> U -> U</span><br />
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> -- we propagate the undefined case</span></div>
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> length _ = U</span></div>
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> -- all other cases return the undefined primitive</span></div>
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span></div>
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> example (B True) x = length x</span></div>
<div style="font-family: inherit;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> example (B False) (N n) = N (n * 2)</span></div>
<div>
<div style="font-family: inherit; font-size: medium;">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> example _ _ = U</span></div>
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">This is less convenient, but it is a syntax issue not one of semantics.</span><br />
<br /></div>
<span class="Apple-style-span" style="font-family: inherit;">Dynamic or static is a langua</span>ge style that is very hard to reconcile, because even if statically typed languages can encode dynamically typed programs you end up having two sub languages that don't talk to each other, an encoded dynamically typed program can't use a function defined in the statically typed side because the statically typed function has many properties expressed via the type system while the dynamically typed program has no static invariant whatsoever. Even if a statically typed language offers a decent encoding of dynamic typing it would be no better than using a dynamically typed language directly. OTOH a dynamically typed language (without a before runtime execution phase) can't offer any of the static typing guarantees and such encoding is impossible by design. This doesn't mean static typing is a fundamentally better approach, it depends on how much are those additional guarantees valued over the cost of having to prove your program to the static type checker.<br />
<br />
Fundamentally dynamically typed languages rely on the existence of undefined behavior, either via failed tag matches, <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">doesNotUnderstand:</span> messages or plain crashes. This same feature exist in most statically typed languages, so it's possible to encode dynamic typing in them, albeit with less syntactic sugar but it adds no value to them. Most dynamic languages reify this undefined behavior and allow it to be inspected at runtime, so a program can work around a undefined behavior which adds a meta-programming feature to the language (e.g. using <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">method_missing</span> in Ruby) but this is orthogonal to the basic idea of allowing programs with undefined paths to be expressed because of the value found in the defined/executable paths.<br />
<br />
Theoretically it's possible to make all behavior defined, you just need to consider all cases in the primitives. For example, <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">if</span> statements/expressions require a <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">boolean</span> but many dynamic languages have the concept of <a href="http://devblog.avdi.org/2011/05/30/null-objects-and-falsiness/">truthiness</a> so one can use anything in the test part of the <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">if</span> and it'll never fail at runtime with some sort of undefined behavior error. You can extend this to all primitives (e.g. arithmetic operators return their unit when presented with invalid values, attribute accessing returns <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">Nil</span> for undefined attributes) and end up with a program that won't crash but may do very unexpected things. This language is equivalent to using <span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">on error resume next</span> in classic VB.<br />
<br />
There's research on <a href="http://ecee.colorado.edu/~siek/gradualtyping.html">gradual typing</a> which tries to provide a single type system with static and dynamic parts with minimal overhead. The results from this research is very encouraging as it would allow a program to have static guarantees over some areas and not over others, which can be very useful for some forms of programming.Danielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.com7tag:blogger.com,1999:blog-4614454413380107813.post-25020907144633278752012-02-26T11:36:00.000-03:002012-05-03T09:33:24.821-03:00Using laziness to improve the performance of Haskell programs<span style="background-color: white; font-family: Arial, sans-serif; line-height: 18px;">To improve the performance of a program the only solution is to reduce the amount of work it does. In Haskell we have three options:</span><br />
<br />
<ol>
<li><span style="background-color: white; font-family: Arial, sans-serif; line-height: 18px;">Replace an algorithm and/or data structure by one with performance characteristics more suited to our problem. It'll work less because the algorithms work less.</span></li>
<li><span style="background-color: white; font-family: Arial, sans-serif; line-height: 18px;">Add strictness to the program so it don't unnecessarily delay computations. It'll work less by not working on thunk creation and such.</span></li>
<li><span style="background-color: white; font-family: Arial, sans-serif; line-height: 18px;">Add laziness to the program so it don't do unnecessary computations. It'll work less by not doing some work that will never be used.</span></li>
</ol>
<div>
<span style="font-family: Arial, sans-serif;"><span style="line-height: 18px;">Option 1 is usually the only one available in strict programming languages. Option 2 is the usual candidate when Haskell people are talking about improving performance. Option 3 is known, but as it seems counter intuitive when we're trying to optimize for performance we tend to forget about it. It's a great tool to use in some situations and it's always good to think about it.</span></span></div>
<div>
<span style="font-family: Arial, sans-serif;"><span style="line-height: 18px;"><br /></span></span></div>
<div>
<span style="font-family: Arial, sans-serif;"><span style="line-height: 18px;">Suppose we have, inside our program, a function that checks some property of a data structure and depending on the result of this property we branch the flow. Let's say we use the following property:</span></span></div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><span style="line-height: 18px;">prop xs = length xs > 2</span></span></blockquote>
<div>
<span style="line-height: 18px;"><span style="font-family: Arial, sans-serif;">If the list has at least three elements the property is </span><span style="font-family: 'Courier New', Courier, monospace;">True</span><span style="font-family: Arial, sans-serif;">, otherwise </span><span style="font-family: 'Courier New', Courier, monospace;">False</span><span style="font-family: Arial, sans-serif;">. The problem here is we <a href="http://en.wikipedia.org/wiki/Fold_(higher-order_function)">fold</a> the entire list to find its </span><span style="font-family: 'Courier New', Courier, monospace;">length</span><span style="font-family: Arial, sans-serif;">. Thanks to laziness we are only going through <a href="http://en.wikipedia.org/wiki/Cons#Lists">the spine of the list</a> not the actual elements (which may do expensive computations on their own) but it's a waste to do all this work to check if the list has at least three elements. The following program does the same computation and works much less:</span></span></div>
<div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><span style="line-height: 18px;">prop (_:(_:(_:_))) = True</span></span></blockquote>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><span style="line-height: 18px;">prop _ = False</span></span></blockquote>
</div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><span style="line-height: 18px;">The pattern only traverses at most three conses of the list. Testing both versions in <a href="http://www.haskell.org/haskellwiki/GHC/GHCi">GHCi</a> demonstrate the performance improvement. It seems a fact of life that these transformations are necessary, but actually this is due to some unnecessary strictness outside our program.</span></span></div>
<div>
<span style="line-height: 18px;"><span style="font-family: Arial, Helvetica, sans-serif;"><br /></span></span></div>
<div>
<span style="line-height: 18px;"><span style="font-family: Arial, Helvetica, sans-serif;">We only need to write down this new version because </span><a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Data-List.html#v:length"><span style="font-family: 'Courier New', Courier, monospace;">length</span></a><span style="font-family: Arial, Helvetica, sans-serif;"> returns an </span><a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Prelude.html#t:Int"><span style="font-family: 'Courier New', Courier, monospace;">Int</span></a><span style="font-family: Arial, Helvetica, sans-serif;"> which is a <a href="http://www.haskell.org/ghc/docs/6.10.3/html/libraries/ghc-prim/GHC-Prim.html#1">strict, unboxed, value in GHC</a>. So to check if </span><span style="font-family: 'Courier New', Courier, monospace;">length xs > 2</span><span style="font-family: Arial, Helvetica, sans-serif;"> we need to compare two strict values which need to be fully evaluated, so </span><span style="font-family: 'Courier New', Courier, monospace;">length</span><span style="font-family: Arial, Helvetica, sans-serif;"> must be fully evaluated.</span></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><span style="line-height: 18px;"><br /></span></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><span style="line-height: 18px;">Now that we found the culprit, what can we do? As usual we are saved by theory and it's <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">paladin</a>. Let's digress a bit and find a lazier number representation.</span></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><span style="line-height: 18px;"><br /></span></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><span style="line-height: 18px;">The length of a list is natural number, not an integer. There's no list with negative length, it makes no sense. If we use the <a href="http://en.wikipedia.org/wiki/Peano_axioms">Peano axioms</a> to express natural numbers we end up with the following datatype:</span></span></div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">data N = Z -- A natural N is either zero (Z)<br /> | S N -- or the sucessor of a natural (S N)</span></blockquote>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">Naturals have a <a href="http://en.wikipedia.org/wiki/Total_order">total order</a>:</span></div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">instance Ord N where<br /> Z <= _ = True<br /> _ <= Z = False<br /> S x <= S y = x <= y</span></blockquote>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">This formulation of the naturals is as lazy as we need. The comparison will only go as far as it needs, until we reach a zero on either side.</span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><br /></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">Now we restate the property, but using </span><a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Data-List.html#v:genericLength"><span style="font-family: 'Courier New', Courier, monospace;">genericLength</span></a><span style="font-family: Arial, Helvetica, sans-serif;"> instead of </span><span style="font-family: 'Courier New', Courier, monospace;">length</span><span style="font-family: Arial, Helvetica, sans-serif;"> and using our natural number formulation (assume the usual </span><span style="font-family: 'Courier New', Courier, monospace;">Eq</span><span style="font-family: Arial, Helvetica, sans-serif;"> and </span><span style="font-family: 'Courier New', Courier, monospace;">Num</span><span style="font-family: Arial, Helvetica, sans-serif;"> instances for </span><span style="font-family: 'Courier New', Courier, monospace;">N</span><span style="font-family: Arial, Helvetica, sans-serif;">):</span></div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small; line-height: 18px;">prop xs = genericLength xs > (2 :: N)</span></blockquote>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">Now the strictness problem disappears. If we think about this a bit we'll realize our earlier performance improvement is isomorphic to this, because the spine of a list is isomorphic to the natural numbers.</span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><br /></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">Let that sink in for a while.</span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><br /></span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;">If we write prop using naturals, but in the second form we have this:</span></div>
<blockquote class="tr_bq">
<span style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">prop xs = case (genericLength xs :: N) of<br /> (S (S (S _))) = True<br /> _ = False</span></blockquote>
<div>
<div>
<span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;">The only difference in the patterns is we're using </span><span style="background-color: white; font-family: 'Courier New', Courier, monospace; font-size: x-small; text-align: -webkit-center;">S x</span><span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;"> instead of </span><span style="background-color: white; font-family: 'Courier New', Courier, monospace; font-size: x-small; text-align: -webkit-center;">_:x</span><span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;">. Remembering that </span><span style="background-color: white; font-family: 'Courier New', Courier, monospace; font-size: x-small; text-align: -webkit-center;">_:x</span><span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;"> means we care only about the shape of the list not its contents it becomes clear that empty lists are equivalent to zero and a cons is equivalent to a successor.</span></div>
<div>
<span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;"><br /></span></div>
<div>
<span style="background-color: white; font-family: Arial, Helvetica, sans-serif; text-align: -webkit-center;">Our optimization was just stating in long form the isomorphism between the spine of a list and natural numbers.</span></div>
<div>
<span style="font-family: Arial, Helvetica, sans-serif;"><br /></span></div>
<div>
</div>
</div>Danielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.com1tag:blogger.com,1999:blog-4614454413380107813.post-13218873544298305922011-12-20T19:52:00.003-02:002011-12-20T19:58:26.989-02:00Understanding higher-order code for free<br />
Recently <a href="http://about.me/missingfaktor">Rahul Goma Phulore</a> <a href="http://twitter.com/#!/missingfaktor/status/148853427479384065">asked</a> for an intuition to understand the Haskell expression:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) ∙ take</span></blockquote>
In Haskell both <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(f ∙)</span> and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ g) </span>are syntactic sugar for <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(λg → f ∙ g)</span> and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(λf → f ∙ g) </span>respectively. These are called <a href="http://www.haskell.org/haskellwiki/Section_of_an_infix_operator">sections</a>.<br />
<br />
Interestingly either sections or function composition alone are pretty easy to grasp, but when combined become food for sphinxes' enigmas.<br />
<br />
<a href="http://apocalisp.wordpress.com/">Runar Oli</a> gave a couple of <a href="http://twitter.com/#!/runarorama/status/148854111247409152">excellent</a> <a href="http://twitter.com/#!/runarorama/status/148854219783417857">answers</a> for his particular question, but I thought this is a good example to walk through some beauties from logic and higher-order types. We could try to look at this code and build some sort of intuitions based on <a href="http://www.haskell.org/haskellwiki/Monad_tutorials_timeline">spacesuits or burritos</a>, but instead we can follow the golden road of logic and exploit a well known fact about programs and types. The <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard isomorphism</a> states that types are isomorphic to theorems and programs are isomorphic to proofs, so whenever we have a type and a program implementing that type the program is a proof of whatever theorem the type represents. Usually a type is much more general than the particular program we're writing so the type doesn't capture the entire semantics of our program. In a sense this is not good situation, because our program depends on a stricter semantics than the types give, but I'll ignore this conundrum for now and instead focus on the types as theorems bit.<br />
<br />
Once we start seeing types as theorems we can apply other results from logic to our problem. For example, if we know our theorem is related to a another theorem (e.g. it implies something else) than we can exploit the results of the related theorem. In the excellent paper <a href="http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html">Theorems for Free</a> Wadler shows that parametricity gives us many useful theorems because we can't produce polymorphic values ex nihilo. Suppose you have the following type:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">f ∷ a → a</span></blockquote>
Ignoring the implementation (don't even try to think about it) what it says about f, what is this theorem? For starters, it's a valid, tautological, implication that states "a implies a". Also it states that there exists a program, such that if you give it something that is a proof of a theorem it'll return something that is a proof of the same theorem, for all possible theorems imaginable. Let's that thought sink for a while: for all possible theorems imaginable.<br />
<br />
There is only one proof that is valid for all theorems, a proof that exploits a loophole in the given logic system (if such loopholes exist) and proves anything. In Haskell this loophole is <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span> (i.e. bottom) the value that inhabits all types, in other words the proof for all theorems. <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span> can manifest in many guises, but essentially it's due to non-termination: all programs that fail to terminate are isomorphic to bottom and can be used to prove any theorem. Any <a href="http://en.wikipedia.org/wiki/Turing_completeness">Turing-complete</a> language suffers from this problem. We can ignore <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span> even in Haskell because <a href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232">fast and loose reasoning is morally correct</a>, so we'll pretend it doesn't exist for the rest of this post.<br />
<br />
Ignoring <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span>, in all forms, we can see that there's only a proof that's isomorphic to any given proof, namely the same given proof. In other words, the only program implements <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">a → a</span> is the identity:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">λx → x</span></blockquote>
For more complex types we can have many possible proofs, which means the type is more lenient than our program and if we depend on the program semantics we may find some bugs later when we change the program and it still type checks but it no longer does what we want. Let's take a look on the type of a function we're interested in:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat ∷ a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a]</span></blockquote>
It states that for all proofs it'll return a list of equivalent proofs. A list is either empty or an element followed by a list:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">data List a = Empty | Cons a (List a)</span></blockquote>
We can encode algebraic data types as explicit <a href="http://blog.lab49.com/archives/3011">sums of products</a>. Ignoring the labels the above is equivalent to:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">data List a = () + (a </span><span class="Apple-style-span" style="background-color: white;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">×</span></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> List a)</span></blockquote>
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">()</span> is the unit of our algebra, if we see List as a logical term, then the equivalent of unit is <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊤</span> (i.e. true, in this formulation we can view <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span> as false, which only means our proof proves nothing). We can also use conjunction <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∧</span> as <span class="Apple-style-span" style="background-color: white;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">×</span></span> and disjunction <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∨</span> as <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">+</span>:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">data List a = </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊤</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∨</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> (a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∧</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> List a)</span></blockquote>
A list is either a trivial theorem or the conjunction of a theorem with itself. A list is not a very interesting theorem, but the proofs represented by lists are more interesting. Going back to our example, repeat is a theorem that states "a theorem implies either <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊤</span> or itself", which is also not much interesting. Which kinds of proofs can satisfy this theorem (i.e. type check)? Below are some choices:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat x = [] -- ignores the given proof and returns the empy list<br />repeat x = [x] -- returns a singleton list with the given proof<br />repeat x = [x,x] -- a list with the proof twice<br />repeat x = ... -- and so on</span></blockquote>
Actually as the list theorem is isomorphic to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊤</span> or a conjunction of any number of copies of a theorem, we can clearly see that it is isomorphic to the pair of a theorem and a natural number, so all possible proofs of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span> are lists containing any natural number of copies of a proof. This is all neat but the most important thing about this is a free theorem stating that <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span> will return either the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[]</span> or a list of a number of copies of the given element. It can't produce the elements of the list <a href="http://en.wikipedia.org/wiki/Ex_nihilo">ex nihilo</a>, they must all be equal to the given element.<br />
<br />
Going further let's see the type of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat)</span>:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat) ∷ ([a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> (a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b)</span></blockquote>
It takes a function, an <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">a</span> and returns a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span>. The function takes a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[a]</span> and returns a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span>. Now it's easier to see what it's doing. <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat)</span> can't produce proofs of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span> ex nihilo, it must use the given function (remember we disallowed <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊥</span>, so it can't just diverge). What are possible possible proofs that satisfy this theorem:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) = λf → λx → f []</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) = λf → λx → f [x]</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) = λf → λx → f [x,x]</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) = ... -- and so on</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><br /></span></blockquote>
<div>
The pattern is identical to the pattern saw in the possible implementations of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span>, which is either surprising or unsurprising, depending on how it fancies you. The main difference is that <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span> just returned the value (i.e. <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[]</span> or <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[x]</span> or ...) and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat)</span> takes a function and applies it to the value.<br />
<br />
Let's see the type of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take</span>:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take ∷ Int → [a] → [a]</span></blockquote>
This theorem has a few possible proofs:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take = λn → λxs → []<br />take = λn → λxs → xs<br />take = λn → λxs → case xs of {[] → []; (x:_) → [x]}<br />take = ...</span></blockquote>
<div>
None of these implementations do what we expect from take but all type check (i.e. prove the theorem). Now we're seeing how flimsy our types are, but it's mostly because we expect too much from general theorems. Either way, we have the same free theorems here, the resulting list will either be <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[]</span> or contain only elements from the original list. This free theorem comes from the parametricity of take, every parametric function has some related free theorem.<br />
<br />
Now what is the type of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take)</span>?<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> take) ∷ (([a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a]) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> Int </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b</span></blockquote>
It looks familiar to the type of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat)</span> doesn't it? Actually we can make it more similar, let's first contrast the types of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span> the partially applied <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take</span>:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat ∷ a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a]<br />take 1 ∷ [a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a]</span></blockquote>
Both have the same structure and their sections also look similar:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> repeat) ∷ ([a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> ( a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b)<br />(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> take 1) ∷ ([a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> ([a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b)</span></blockquote>
It seems that taking the right section of a function will take it inside out and "promote" types in both sides of the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span> to functions to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span>. You can see this a CPS transform of the function, with the continuation as the first argument.<br />
<br />
As with <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat)</span>, <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take 1)</span> has more interesting free theorems, relating on how it can produce <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span> from <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[a]</span>. In most higher order compositions the number of free theorems increase, because we (usually) have more parametricity and the universal quantitification limits how we can compose those.<br />
<br />
Dissecting <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> take)</span> type we see that it takes a higher-order function an <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">Int</span> and returns a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span>. Let's see some possible proofs for this theorem:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take) = λf → λn → f id<br />(∙ take) = λf → λn → f (const [])<br />(∙ take) = λf → λn → f (λxs → case xs of {[] → []; (x:_) → [x]})<br />(∙ take) = ...</span></blockquote>
</div>
<div>
Like what happened with the possible <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat)</span> proofs we are mainly repeating the possibles proofs for take and making it higher-order. We can fake some but not much, namely we can return <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[]</span> (which are trivial due to being isomorphic to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">⊤</span>) or we can pick some elements from the list, but we can't produce elements ex nihilo and we must call <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">f</span> (i.e. our continuation).<br />
<br />
We can read the type of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take)</span> as "Given a function that uses mappings from lists to lists to produce something and an int it'll return something". Whatever <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> take)</span> does is limited to look at an <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">Int</span> an to provide a function of type <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[a] </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a]</span>. <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">f</span> can ignore the function provided by <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">∙</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> take)</span> or use it but it must provide a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span>.<br />
<br />
Finally let's look at our original enigma. First we can use the right section of take to make everything prefix:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) ∙ take = (∙ take) (∙ repeat)</span></blockquote>
Remembering the types of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat)</span> and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take)</span> we can use the basic application rule to find the resulting type (with some unification):<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat) ∷ ( [a] → b ) → (a → b)<br />(∙ take) ∷ (([a] → [a]) → c ) → Int → c</span></blockquote>
</div>
<div>
As we apply <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take)</span> to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ repeat)</span> we unify <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">b</span> with <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[a]</span> and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">c</span> with <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> b)</span>, which is <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(a </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a])</span>, and we end up with:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(∙ take) (∙ repeat) ∷ Int → (a → [a])</span></blockquote>
This final type has the same free theorems as <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take</span> and <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span>, namely it will either return <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">[]</span> or a list with some number of copies of the same element.<br />
<br />
Most of this exercise may seem pointless but it's mostly due to the uninteresting list theorem and, consequently, to the uninteresting <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take</span> theorem. With some dependent type encoding the length of list we could have a much stronger (and less general) theorem for <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">take</span> and even <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">repeat</span> would be a bit more interesting.<br />
<br />
The relation of right sections to continuations is more relevant to understand the types and how these combinators work. A left section it's the reverse, the result is the continuation of something, instead of expecting a continuation:<br />
<blockquote class="tr_bq">
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">(repeat ∙) ∷ (b </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> a ) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> (b </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a])<br />(uncurry take ∙) ∷ (b </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> (Int, [a])) </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> (b </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">→</span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> [a])</span></blockquote>
<div>
Here I used <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">uncurry</span> to make the correspondence between the types clearer in this case. The reasoning is similar and left as an exercise for the reader.</div>
</div>
</div>Danielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.com0tag:blogger.com,1999:blog-4614454413380107813.post-87747808266344407672011-11-23T20:17:00.000-02:002011-11-23T20:17:20.464-02:00Understanding Object SystemsThere are some regular discussions on programming that are quite boring, but from time to time you can find new thoughts lurking there. Using ideas from <a href="http://en.wikipedia.org/wiki/Theory_of_Constraints">Theory of Constraints</a> we can model conflicts in a way that the apparent dichotomy <a href="http://en.wikipedia.org/wiki/Core_Conflict_Cloud">evaporates</a> and a better way presents itself.<br />
<br />
The particular dilemma I was looking at was the <a href="http://gbracha.blogspot.com/2009/10/image-problem.html">Smalltalk's image problem</a>, actually not any of the problems described there but the usual spiel about how images are against the Unix way and such. The essence of the argument boils down to "I want to manipulate Smalltalk code as source files like everything is done in the Unix way" (many times people just talk about how Vim or Emacs is much better than the <a href="http://en.wikipedia.org/wiki/Smalltalk#Image-based_persistence">image</a>, but the problem goes a little deeper than that) which is an enormous flag indicating that the person probably doesn't understand how Smalltalk works (<a href="http://blog.blainebuxton.com/2005/07/source-code-in-files-how-quaint.html">"Source code in files? How quaint."</a> -- Kent Beck). OTOH the <a href="http://www.faqs.org/docs/artu/">Unix way</a> is also a cornerstone of software engineering so this isn't a <a href="http://www.dreamsongs.com/WorseIsBetter.html">worse is better</a> scenario but a true indicative that something very important is missing.<br />
<br />
It occurred to me a way to solve this dilemma, just expose the image as a mount point (e.g. using <a href="http://fuse.sourceforge.net/">FUSE</a>), with methods as files inside classes (directories) with categories and protocols as directories with links to the methods/classes and special links like super also provided. As it happens with all good ideas <span id="goog_691330563"></span>there<span id="goog_691330564"></span> should be already something on the internet, so I used my google-fu and found exactly what I wanted on a <a href="http://www.cincomsmalltalk.com/userblogs/travis/SingleView.ssp?showComments=true&forPrinter=true&entry=3369006577">FUSE based Smalltalk</a> description (which unfortunately didn't lead me to actual software to play with). It even described the kind of integration with the live image I was thinking about (e.g. changing a method file and reflecting the change in the image) which is really cool. It's interesting to see this concept isn't used by all Smalltalkers around the globe to respond to these complaints so either is fundamentally flawed or there is something missing. Looking through the search results I also found many pointers to <a href="http://forum.world.st/stash-a-Smalltalk-shell-or-what-happens-when-you-let-your-mind-wander-in-the-shower-td3076953.html">Smalltalk shells</a> or <a href="http://wiki.squeak.org/squeak/1914">shells in Smalltalk</a> which are the same underlying idea presented in a different way (the <a href="http://forum.world.st/stash-a-Smalltalk-shell-or-what-happens-when-you-let-your-mind-wander-in-the-shower-td3076953.html">Stash</a> idea is also very close to this).<br />
<br />
In Unix we have (or should have, Plan 9 got this right, but I digress) everything as a file, so we can see processes as files and such. In Smalltalk everything is an object so it should be just a matter of changing the UI to bridge the two concepts. Going further, having every object as an executable file and being able to send messages directly to it (e.g. <span class="Apple-style-span" style="background-color: #eeeeee; font-family: 'Courier New', Courier, monospace; font-size: x-small;">#12ab76e9 at: 1 put: 'Hello World'</span> would send the <span class="Apple-style-span" style="background-color: #eeeeee; font-family: 'Courier New', Courier, monospace; font-size: x-small;">at:put:</span> message to the object identified by the hash <span class="Apple-style-span" style="background-color: #eeeeee; font-family: 'Courier New', Courier, monospace; font-size: x-small;">#12ab76e9</span>. With a proper mount and some path extensions we could do almost everything in Unix, without having to reinvent the shell in Smalltalk.<br />
<br />
This solves the source code in files problem, as you can mount your image and use VI, sed, git, etc., to manipulate the definitions. You can even manipulate the image from the shell, implementing a polymorphic mkdir that does the right thing when it's a class or a category. It looks like a wonderful idea, or isn't? Is it too good to be true?<br />
<br />
In software I believe there are two problems that every idea should solve before becoming something useful:<br />
<br />
<ol>
<li>Does it work in theory? You need to really think things through, many times there are theoretical barriers that make a nice idea fail badly in practice.</li>
<li>Is it feasible in practice? How much effort you need to make it work? Measure this in <a href="http://projects.csail.mit.edu/gsb/old-archive/gsb-archive/gsb2000-02-11.html">yaks</a>.</li>
</ol>
<div>
It seems to be workable in theory so I fear it's unfeasible in practice, after all the Smalltalk images are built around the GUI, so it may require some serious yak shaving to untangle some bits (probably like all software projects it'll work almost right and then become almost impossible). But I think it's a worthwhile project and it would help greatly on explaining how object systems actually work.</div>Danielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.com2tag:blogger.com,1999:blog-4614454413380107813.post-50147722903337091802011-08-20T15:55:00.000-03:002011-08-20T15:55:11.372-03:00What is the meaning of source code?<span class="Apple-style-span" style="font-family: inherit;">Today I was thinking about literals in source code and what is their meaning. I ended up in a conversation with <a href="http://twitter.com/#!/msimoni">@msimoni</a> and we were talking past each other, so I figured out it was better to write it down anywhere.</span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">Let's start with a language based on the untyped <a href="http://en.wikipedia.org/wiki/Lambda_calculus">lambda calculus</a>, the syntax is pretty simple:</span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> e = x </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">| </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"><span class="Apple-style-span" style="line-height: 19px;">λx.e</span></span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;"> </span><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace; font-size: x-small;">| e e</span><br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">It's not the most pleasant syntax (although is many times better than the Turing machine) to program. So we decide to add some sugar on top of it: data-types, special forms, literals, etc.. Hopefully we define these on the calculus primitives and the language does not become more complex to reason. </span>Essentially the meaning of the additional syntax is their translation to the calculus. Now we have two choices: either we add this sugar as special syntax or we bake some form of syntax extensibility in the compiler/interpreter/front-end. Before we go down this road I'll digress a bit and talk about source code.<br />
<br />
Most languages use source code as a way to express programs and as an input to compilers/interpreters, but when we start viewing it as one representation of the program we need to define what a program is. Eventually we'll use some syntax (usually the same) to denote the program's meaning, but we need to think of the program as an object we can manipulate instead of text to be fed to the compiler. If we're going to store and render the program we don't need to use the same forms for both needs. Lets talk about a concrete issue, how do we store and represent numbers.<br />
<br />
If we encode naturals in our language using <a href="http://en.wikipedia.org/wiki/Church_encoding">Church encoding</a> we can easily render 2 to the programmer and accept it as a valid input, while we store the program using the complete encoding (i.e. <span class="Apple-style-span" style="font-family: monospace, 'Courier New'; font-size: 13px; line-height: 19px;">λf.λx.f (f x)</span>). We can even represent <span class="Apple-style-span" style="font-family: monospace, 'Courier New'; font-size: 13px; line-height: 19px;">λx.2+x</span> while internally keeping it as the expanded form (left as an exercise to the reader :). Of course this way makes the storage less efficient than it could be which leads us to the first observation: literals are just compression mechanisms. They work as compression for both the compiler/interpreter and for us (as it's simpler to read/write 2 than the equivalent encoding). If we just store the encoded number though we need to also keep something to remind us to compress it to 2 when rendering it, we could rely on pattern matching and equational reasoning but we'll find out that many compression schemes work with the same encoding (e.g. the user would see either the number 2 or part of data structure).<br />
<span class="Apple-style-span" style="font-family: inherit;"><br /></span><br />
<span class="Apple-style-span" style="font-family: inherit;">Viewing it in this light we can go back to literals with a new perspective, our language can have a limited set of literals with built-in encoders or have a simpler literal form and an extensible encoding mechanism. Most languages go the first way but the libraries' programmers end up using strings and some parsing or <a href="http://c2.com/cgi/wiki?EmbeddedDomainSpecificLanguage">EDSLs</a>. If we go the second way we end up with LISP-like macros for literals. Even if the language is going to have a fixed set of literal forms it's better to have almost no intelligence in these than to add support for many specific concerns. For example, it's better to have plain string literals without any embedded escaping mechanism than to have escaping for special characters (that are only special because of the escaping concerns) and to support mechanisms to control terminals or do layout (e.g. \n and friends).</span><br />
Danielhttp://www.blogger.com/profile/05150497263726512307noreply@blogger.com0