Church vs Curry Types

Summary: Static vs dynamic typing debates often flounder because the debators see from two different perspectives without knowing it. Learning to identify the two perspectives can calm the discussion. The tension between the two perspectives has led to Gradual Typing and other technologies.

Many discussions about type systems around the internet fail to be interesting because one or both parties are not versed in type theory. There's a less common (yet related) reason, which I have begun to notice more and more: people who are not familiar with the difference between Church Types and Curry Types. These are also known, respectively, as Intrinsic Types and Extrinsic types. Because the participants are not aware of the two perspectives, they blame the other one for ignorance, when in fact they just have a different perspective.

Church Types are what Haskell has. Church types are named for Alonzo Church, the inventor of the lambda calculus. In a Church-style system, types are an intrinsic part of the semantics of the language. The language would be different without the types--it may even be meaningless. With an intrinsic type system, the meaning of the program is different from the runtime behavior of the program. One way to think of this is that so much of the meaning of the program occurs at compile time that you can begin to think of the program having properties you can reason about even if you never run the program.

The other kind of types are Curry types (aka extrinsic types). They are named for Haskell Curry, the man the Haskell language is named after. Curry-style types is when a system of types is applied that is not part of the semantics of the language. This is what Clojure has in core.typed. The meaning of a Clojure program is not dependent on it passing the type checker--it can be run without it. The type checker simply alerts you to type errors in your code. Note that you could consider your type checker to be your own head, which, as flawed as it may be, is what most Clojure programmers use. The types could be anywhere outside of the language.

Each perspective is valuable and bears its own fruit. Intrinsic types are great because you are guaranteed to have a mathematically-sound¹ safety net at all times. You always have something you can reason about. Such is not guaranteed for extrinsic type checkers. They may not be able to reason about your code at all.

Extrinsic types are useful because you can apply multiple type systems to your code²--or even write something that you don't know how to prove is sound. There are more benefits on both sides, but you get the idea.

We now have a new perspective which is slightly "higher" than either of them. We can now see that both perspectives exist and talk about them as such. What can we see/say now that we couldn't before?

A famous article by Robert Harper exemplifies the Church perspective very well. It argues that untyped programs are a subset of typed programs. They are programs that have a single type and all values are of that one type. So instead of being liberating, dynamic languages restrict you to one type. Notice the assumption that languages have a type system by default which is typical of the Church-style perspective. We can now say "This reasoning is correct given that perspective."

On the other side, you'll often see a dynamic typist say the exact opposite: that well-typed programs are a subset of dynamically typed programs. In other words, well-typed programs are just dynamic programs with fewer errors. Curry-style to the core: static type errors are something that is added onto the semantics of the language. We can now see that they are right, from their perspective.

Here's a diagram:

Church vs Curry Types Language Subset Diagrams

Notice how they're isomorphic? That means something, I just don't know what :)

My ambitious hope is that this perspective will quiet a lot of the fighting as people recognize that they are just perpetuating a rift in the field of mathematics that happened a long time ago. The perspectives are irreconcilable now, but that could change. A paper called Church and Curry: Combining Intrinsic and Extrinsic Typing builds a language with both kinds of types. And Gradual Typing and Blame Calculus are investigating the intersection of static and dynamic typing. Let's stop fighting, make some cool tools and use them well.

You might also like

• Hindley-Milner in Clojure
• On Type Unity
• Pre-West Prep: Nathan Sorenson
• Ambrose Bonnaire-Sergeant interviewed about Typed Clojure

CSS has Weak Forms of Abstraction and Combination

Summary: According to the requirements proposed by Abelson and Sussman, CSS does not provide adequate means of combination and abstraction to be considered a powerful language.

I am trying to improve the maintainability and reusability of my CSS over the longterm. I've written about how to organize CSS before. I've learned a lot since I wrote that. I've tried lots of things and talked to lots of people, I finally seem to have found a conceptual framework to capture my new understanding. I'm trying to explore it here. Comments are welcome.

I'm going to take a cue from the first page of SICP and analyze CSS as a language.

Abelson and Sussman in SICP 1.1 (italics mine):

A powerful programming language is more than just a means for instructing a computer to perform tasks. The language also serves as a framework within which we organize our ideas about processes. Thus, when we describe a language, we should pay particular attention to the means that the language provides for combining simple ideas to form more complex ideas. Every powerful language has three mechanisms for accomplishing this:

primitive expressions, which represent the simplest entities the language is concerned with,

means of combination, by which compound elements are built from simpler ones, and

means of abstraction, by which compound elements can be named and manipulated as units.

Let's analyze CSS in terms of these three mechanisms.

Primitive Expressions

The simplest entities the language is concerned with are properties and primitive selectors. CSS properties, though they have a property name and property value part, are meaningless if split up. Primitive selectors include element name selectors (body, a, div), class name selectors (.main-wrapper), id selectors (#login-form), and pseudo-class selectors (:hover), among others. Properties appear inside the rule body ({}), while selectors appear before the rule body. The two are semantically and syntactically separated.

Means of Combination

Properties can be combined in two ways. First, multiple properties can be put inside the same rule body. This is the most obvious and most readable form of property combination. The second form is harder to reason about. It occurs automatically within the browser during rendering. That form of combination, involving the application of multiple rule bodies to the same HTML element, uses a complex ordering of properties from all bits of CSS and element styles on the page.

Tomes have been written about how difficult it is to reason about this automatic form of combination. Usually, the answer is limiting it (or avoiding it altogether) through programmer discipline, with varying degrees of success.

Primitive selectors can be combined in several ways. Without spaces between them, multiple selectors will intersect, meaning they target elements more specifically. div.main-container will target div elements that ALSO have the class main-container.

With spaces, multiple selectors indicate nesting. div .main-container matches any element of class main-container within any div. There are several operators which combine them in different ways (> indicates direct nesting, etc.). Nested selectors are associated with CSS that is strongly coupled with the structure of the HTML it is styling and therefore less reusable.

Selectors that are combined with commas create a group. These compound selectors will match any element that matches at least one of the component selectors. header, .header will match all header elements and all elements with class header.

There are more types of selector combintation operators, but they are more specialized and less frequently used.

The locus of combination, for both properties and selectors, is the rule. The rule has one compound selector and zero or more properties. Rules with zero properties have no effect.

Means of Abstraction

The means of abstraction in CSS are quite limited. There is no way to name anything. People lament the lack of named values (often refered to as variables) or named styles (sometimes called mixins). Naming is out in CSS.

The only means of abstraction is the class and id, which are labels that can be applied to HTML elements. With an id or class (or combinations), you can target precisely the elements you need to and achieve some reuse. For instance, I can "reuse" the #login-form id selector in two different rules. I can also add the class rounded-corner to two different HTML elements, effectively "reusing" the same rule twice. By a very disciplined use of class selectors by combining them with commas, one can apply "rule bodies" as a unit in a very limited way, though it is impracticable in practice.

The disadvantage to this technique of using id and class selectors is that the HTML must be modified when styles change, defeating the purpose of using CSS for content/style separation. There is a lot of discussion about using semantically named classes. For instance, call the button login-button instead of green-shiny-button. This is thought to be more robust in the face of style changes, but requires existing CSS to be thrown away in order for the page to be redesigned. CSS offers no good way to modify HTML and CSS independently.

Conclusion

CSS does not meet the criteria for a "powerful language" as used in SICP. This is no surprise. The reasonable means of combination are limited to the rule. The means of abstraction are almost non-existent. There is no way to name anything. And the other form of abstraction (ids and classes) provides no way of reusing both the HTML and the CSS. It is obvious why CSS is typically unmaintainable. With the current crop of compile-to-CSS languages (commonly known as "CSS Preprocessors"), there is hope that better means of abstraction are possible. How will compile-to-CSS languages fare in this same analysis?

You might also like

• Separation, Abstraction, and Cascading in CSS
• LESS has Better Forms of Abstraction than CSS
• Pre-West Prep: Priyatam Mudivarti
• Separation of Presentation and Content

LESS has Better Forms of Abstraction than CSS

Summary: LESS has obviously better forms of abstraction and combination than CSS. It has recursive style definitions, which is enough to consider it a "powerful language".

Ok, it's obvious that CSS has weak forms of combination and abstraction. But now we have a good framework for understanding why. "CSS Preprocessors", as they are called, are getting really popular now. We would be smart to analyze LESS in the same way that we analyzed CSS, if only to temper the glamor of trendiness that surrounds it. Comments are welcome.

Because LESS aims to be a superset of CSS, it has all of the primitive expressions, means of combination, and means of abstraction that come baked into CSS. I already went over those last time, so I will not go over them again. So what things are added by LESS?

Primitive Expressions

Besides existing CSS properties, LESS adds two new primitive expressions. Mixin application (.rounded-corners(10px);) in a rule recursively applies the primitive expressions defined in the body of the mixin to the current rule. Mixin applications can be parameterized with value expressions, or they can have no parameters. Extension (&:extend(.blue-button);) is similar, but instead of applying the primitive expressions to a rule body, it adds the selector of the rule to the rule selector of the extension. Extension is recursive as well.

Variables and mathematical expressions change the way primitive properties work. In CSS, primitive properties were comprised of a property name and a literal property value. In LESS, variables and math expressions, as well as literal values, can be in the value place (right hand side) of a property.

Variables can also be used in selectors.

Means of Combination

The principle means of combination are still the rule, but add to it the ability to nest rules, and things are more interesting. Nesting two rules is shorthand for writing out two rules (unnested) with a nested selector. While in the simple case it is simply a shorthand, when nested rules are applied as mixins, you gain a lot more than better syntax. Mixins with nested subrules allows you to name a nesting and refer to it later.

Means of Abstraction

CSS did not contain much in the way of abstraction. LESS focuses primarily in the realm of abstraction, probably to appease the will to power of front-end designers. Variables allow property values to be named, and naming is a form of abstraction. Variables are a good way to name values that all have the same meaning and would therefore change at the same time. For instance, a shade of green that is used throughout the styles is a perfect use for variables. Variables can be used in a similar way to name selectors.

A more powerful form of abstraction comes from the ability to define mixins, apply mixins, and use of :extend(). In LESS, any rule using a single class or id selector can be used as a mixin. This is essentially a way to name a rule--our principle form of combination. In addition, if you put empty parentheses after the class selector in the rule, the rule is not outputted into the generated CSS, which can save bytes. Mixins can also have parameters (scoped variables), so they can be abstracted over a variety of values. Extend allows a similar kind of abstraction which promises to be more efficient.

Mixins are very powerful. In fact, this is the kind of abstraction that is needed for LESS to be powerful, as defined by Abelson and Sussman. Because you can now name a group of styles (mixin) and then use that name in another group of styles (mixin application), LESS has full-on recursive style definitions. With extension, it also has recursive selector definitions. In LESS, we can talk of "levels of abstraction" whereas in CSS there was only one.

Conclusion

LESS has recursion. It lets you define and name groups of properties, then refer to those groups by name in other groups of properties. We can consider LESS powerful enough to express useful abstractions. Yet though it is more powerful than CSS, it still has many of the problems of CSS (especially complex rules governing the combination of multiple rules to a single element). How can LESS be leveraged to gain its power but tame its weakness? Is there a subset of LESS that can gerrymander the good parts away from the bad parts?

You might also like

• Separation, Abstraction, and Cascading in CSS
• CSS has Weak Forms of Abstraction and Combination
• Pre-West Prep: Priyatam Mudivarti
• Separation of Presentation and Content

Lisp with Macros is Two Languages

A Lisp with a macro system is actually two languages in a stack. The bottom language is the macro-less target language (which I'll call the Lambda language). It includes everything that can be interpreted or compiled directly.

The Macro language is a superset of the Lambda language. It has its own semantics, which is that Macro language code is recursively expanded into code of the Lambda language.

Why isn't this obvious at first glance? My take on it is that because the syntax of both languages is the same and the output of the Macro language is Lambda language code (instead of machine code), it is easy to see the Macro language as a feature of the Lisp. Macros in Lisp are stored in the dynamic environment (in a way similar to functions), are compiled just like functions in the Lisp language (also written in the Macro language) which makes it even easier to confuse the layers. It seems like a phase in some greater language which is the amalgam of the two.

However, it is very useful to see these as two languages in a stack. For one, realizing that macroexpansion is an interpreter (called macroexpand) means that we can apply all of our experience of programming language design to this language. What useful additions can be added? Also, it makes clear why macros typically are not first-class values in Lisps: they are not part of the Lambda language, which is the one in which values are defined.

The separation of these two languages reveals another subtlety: that the macro language is at once an interpreter and a compiler. The semantics of the Macro language are defined to always output Lambda language, whereas the Lambda language is defined as an interpreter (as in McCarthy's original Lisp paper) and the compiler is an optimization. We can say that the Macro language has translation semantics.

But what if we define a stack that only allows languages whose semantics are simply translation semantics? That is, at the bottom there is a language whose semantics define what machine code it translates to. We would never need to explicitly write a compiler for that language (it would be equivalent to the interpreter). This is what I am exploring now.

You might also like

• Exponential Backoff
• Try Three Times
• When To Use a Macro in Clojure
• Church vs Curry Types

Two Kinds of Bootstrapping

Summary: I like languages with a small core that is extensible. The languages tend to be weird and require less code to bootstrap.

I know of two ways to bootstrap a language.

The first way is probably more traditional. I'll call the first way Type 1. In Type 1, you write a bare-minimum compiler for your language in a host language. So maybe you write a Lua compiler in C. Then you write a Lua compiler in Lua. Then you compile your compiler. Now you have a compiler, written in Lua. You can add to it and modify it without ever having to touch the C code again. You have the advantage of writing the features of your language (Lua) in a higher-level language (Lua). And finally, as you add features to your compiler, you can use those to add more features. There's some leverage.

I like the second way better. I'll call it Type 2. In Type 2, you write a small, powerful set of abstractions in the host language. For instance, you write an object system in C, a stack and dictionary in assembler, or lexical closures in Java. Then you write a compiler that targets those abstractions. If the abstractions are chosen correctly, your compiler is done. You can begin building abstraction on top of abstraction without touching the compiler.

There are a few things to note:

1. Type 2 languages (Lisp, Smalltalk, FORTH) tend to be weird because they were birthed in a different way. The abstractions, though powerful, are often raw.

2. Type 2 languages can be bootstrapped faster. The core is often much smaller than a full-featured compiler.

3. Type 2 languages tend to require less code in general. I guess it's because you're writing most of it in a language that is compounding leverage.

4. Type 2 languages are more easily ported, since all you have to do is rewrite the core. Type 1 languages, depending on how they are built, can require you to re-bootstrap or write a cross-compiler.

In the end, I believe that both Type 1 and Type 2 are viable options for language-building. I prefer Type 2. If Type 2 intrigues you, you should learn Lisp (or FORTH or Smalltalk). I recommend the LispCast Introduction to Clojure videos course.

Learn Functional Programming using Clojure with screencasts, visual aids, and interactive exercises

Learn more

You might also like

• Clojure is Imperative
• Church vs Curry Types
• CSS has Weak Forms of Abstraction and Combination
• LESS has Better Forms of Abstraction than CSS