This is the first in a series I intend to write in regard to the syntax of Ancient Greek hyperbaton, and what can be done about it formally using a combinatory categorial grammar. We will begin with a pathological example of Y1 hyperbaton from Sophocles’ Trachinian Women:
τὴν Εὐρυτείαν οἶσθα δῆτα παρθένον;
the-*acc* of-Eurytus-*acc* know-*2.sing* of-course girl-*acc*
“You of course know the daughter of Eurytus…?” (Trachinian Women, l. 1219)
The six speeches of the Symposium may be divided into two sets: on the one hand, there is Phaedrus’s speech and those which are derivative of his, and on the other hand, there are the novel speeches; and these are the ones which reject the previous approaches and propose unique theories of Eros.
In this paper, I demonstrate how, and to what degree, phrase projectivity corresponds with register and meter in Sophocles’s Antigone, by developing a quantitative metric ℘ for projectivity and comparing it across lyrics, trimeters and anapaests using the data provided by the Perseus Ancient Greek Dependency Treebank. In the appendices, the formal algorithm for the computations done herein is developed in Haskell.
We can define the STLC at the type-level in Haskell, and then provide a type of derivations (proofs of well-typedness) which is indexed by terms. Further, we can use Haskell’s type classes to infer typing derivations for well-typed terms in the STLC.
Vinyl is a general solution to the records problem in Haskell using type level strings and other modern GHC features, featuring static structural typing (with a subtyping relation), and automatic row-polymorphic lenses. All this is possible without Template Haskell.
It is trivial to prove type equality in Haskell (to the extent that anything is every “proved” in Haskell). As for proving type inequality, Conor McBride demonstrates that this is possible to do using type families. Today, I’d like to show some techniques for doing the same in C++ with templates.
Today, I hope to introduce a more lightweight approach to immutable objects in Objective-C that sidesteps some of the problems with class clusters (such as hostility to subclassing) by making some trade-offs. The class cluster approach provides the following fronts of protection against illegal mutation:
- Mutation methods only occur in the interfaces for the mutable variants. This protects us when types are preserved.
- Sending a mutation message to an immutable object results in an exception.
I’m going to argue that the first force of protection (that of types) is far more important than the second (that of runtime exceptions), and that if we are willing to give it up, we can have a vastly simpler notion of immutability and mutability. Finally, I’ll discuss ways we can recover runtime exceptions in the case of an unsafe cast, and finally how we can recover the functionality of -mutableCopy in a subclass-friendly fashion.
Perhaps the greatest sin in the common body of Cocoa design patterns is the pervasiveness of “stringly-typed” code: it frequently comes up in KVO and bindings, among other things. Various macros have arisen to allow type checking of keypaths, largely thanks to efforts by Justin Spahr-Summers and myself. Today, I’d like to talk a bit about some ideas for enforcing statically trusted boundaries for checked keypaths.
In a slight diversion from my path
toward NL semantics in Martin-Löf Type Theory, I'd like to delve
a bit into formulating NL syntax in Coq, a dependently typed theorem
prover based on the Calculus of Inductive Constructions.
In my view, extensible records are a rather good problem for gauging type system expressivity. I recently wrote an extensible records framework for Haskell called Vinyl; today, I thought I would see what it would take to manifest something similar in C++.
There have been various attempts at faking dependent types in Haskell, most notably Conor McBride’s Strathclyde Haskell Enhancement. Since its creation, several improvements to GHC have set the stage for some of SHE’s features to be implemented natively.
Let’s see what’s necessary to fake dependent types with singletons in today’s GHC.
My great joy at finally taking logical semantics for natural language at Berkeley was a bit dampened by the realization that everyone is still doing semantics in a type theory from the 1940s. Rather than wallowing in dismay, I have been inspired to think about manifesting semantics in a modern Constructive theory within the Martin-Löf tradition; this is the first in a series of posts in that vein.
Last time, I showed how ∏ and ∑ types generalize the cartesian power (function arrow) and the cartesian product respectively. Unfortunately, the Agda implementation I provided requires the first element in the ∑ -pair to be a term of a type, which precludes the encoding of existentials which could be used to abstract away a type (which is a term of a kind). Today, I’ll show how to fix this using Universe Polymorphism.
∏ and ∑ are two fundamental connectives of Intuitionistic Type Theory, corresponding to ∀ and ∃ in logic respectively. In their non-dependent special cases, they represent cartesian powers and products respectively. Let’s take a look at how this works!
Previously, I discussed using explicit proof parameters in combination with lifted proof generators in order to write code that can distribute its invariants across static and dynamic phases as appropriate. The major disadvantage to that approach is that it can sometimes be difficult and cumbersome to create proofs of certain properties manually. Today, I’ll discuss how to automate that using type classes.
Unfortunately, Haskell’s Prelude abounds with partial functions, like head, tail, read, etc. There have been some attempts to resolve this by replacing them with safe variants that return Maybe a rather than a. But what about when we can make static guarantees about data?
Because Haskell doesn’t have real ∏ -types, we can’t bring those invariants into our program specifications in the same way a dependently-typed language could. But with GHC 7.4’s new -XDataKinds extension, many data types are automatically promoted into the kind-level; this means that we can maintain a static-dynamic phase distinction at the same time as having data structures mirrored into the kind level. Combined with phantom-types, this is enough to start encoding interesting invariants into the type system. But, reusing statically verified code for dynamic values can be problematic.
Funny how we like to talk about total functions. As if there’s any other kind of function.
This was my somewhat flippant remark this morning, which incited a conversation about the nature of functions and partial functions, leading me to learn a few things.
In February, I wrote about using instancetype to get semi-typesafe collections in Objective-C. After an email conversation with Patrick Beard, I’d like to present another approach.
One sad consequence of protocols only being commonly used to encode delegation is that beginners frequently conflate protocols with delegation. Hence the proliferation of tutorials on how to “do delegates” in Objective-C; in fact, I had written one such tutorial a long time ago, and it became so popular that I deleted it, for it was feeding directly into this very conflation (which I deem damaging to learners).
In this article, I’ll be showing a more interesting use of protocols: typesafe collections.
The latest versions of the Clang compiler extend the Objective-C language with related return types, which allow a limited form of covariance to be expressed. Methods with certain names (alloc, init, etc.) are inferred to return an object of the instance type for the receiver; other methods can participate in this covariance by using the instancetype keyword for the return type annotation.
Typically, this feature is used for convenience constructors which would previously have returned id. However, we can also use it to encode statically-typed collections without full-blown generics.
A monad is just a monoid in the category of endofunctors, what’s the problem? — James Iry.
Building on the work of sigfpe’s From Monoids to Monads and monoidal’s Kind polymorphism in action (which demonstrates kind polymorphism in the Ultrecht Haskell Compiler), we can unify Monoid and Monad under one type class in GHC 7.4.
It’s easy to express pairs in the untyped lambda calculus; adding types makes it somewhat more complex to get a correct encoding. In this article, I explain how we can build a pair with typesafe accessors in a polymorphically typed lambda calculus with type operators (System Fω), and demonstrate it in Haskell. This document is Literate Haskell: simply copy and paste it into an .lhs file, and you can feed it into GHCI.
If you want an NSSlider to snap on certain intervals, your option out-of-the-box is to give it tick marks (using -setNumberOfTickMarks:), and then enforce that it can only be set to values coinciding with a tick mark (using setAllowsTickMarkValuesOnly:). This is great, if you only want to accept values at certain intervals; but it’s not very helpful if you simply want to snap to values at key points (like quarters, or thirds).
In the past, I have railed against companies who choose to write mobile web applications instead of native apps. Having recently tried the mobile version of Pinboard, as well as the new Basecamp mobile version, I must slightly revise my opinion.
I’ve long been frustrated by the complexity of the Class Cluster pattern, and feel that in most cases, it can be replaced with something cleaner and more flexible. JSBag is an example of a new collection class with mutable and immutable variants that is implemented with a pattern similar to the Class Cluster, but far less coupled. I do this using Traits.
A ‘bag’ is a multiset, or a set which can contain duplicate objects. CoreFoundation includes CFBag, which is the same concept; for reasons of simplicity, JSBag was implemented on top of NSArray instead of CFBag, but it certainly would be possible if better performance were desired.
I know people. Some of them are even reading this. You know who you are. The ones who sighed in relief when it became cool to be a geek, when the International Baccalaureate became a source of pride and mutual camaraderie. You’re one of the new generation of movers, shakers and future-makers; but what’s this? You’re hiding?
After having seen the work on Etoilé under GNUstep, I began to fantasize over writing applications for Mac OS X in Smalltalk. Unfortunately, all of the full Smalltalk solutions I have scene are really weird and childish (yeah, I’m looking at you, Squeak), and totally impractical for distributing applications that fit in with Mac OS (yeah, you too, Pharo).
What I really wanted was a version of Smalltalk that used the same object modal as Objective-C, like Pragmatic Smalltalk of Etoilé, or even MacRuby on Mac OS. Most of all, I wanted it to treat me like an adult: I don’t need a class browser, thank you, I’m more comfortable working with plain-old files. The persistent image construct in Smalltalk really makes me uncomfortable.
