How is it possible to write signal handlers in GHC Haskell? After all, the set of system calls allowed inside signal handlers is rather limited. In particular, it is very hard to do memory allocation safely inside a signal handler; one would have to modify global data (and thus not be reentrant), call one of the banned syscalls (brk, sbrk, or mmap), or both.
On the other hand, we know that almost any Haskell code requires memory allocation. So what’s the trick?
The trick is that a Haskell handler is not installed as a true signal handler. Instead, a signal is handled by a carefully crafted RTS function generic_handler (rts/posix/Signals.c). All that function does (assuming the threaded RTS) is write the signal number and the siginfo_t structure describing the signal to a special pipe (called the control pipe, see GHC.Event.Control).
The other end of this pipe is being watched by the timer manager thread (GHC.Event.TimerManager). When awaken by a signal message from the control pipe, it looks up the handler corresponding to the signal number and, in case it’s an action, runs it in a new Haskell thread.
The signal handlers are stored in a global array, signal_handlers (GHC.Conc.Signal). When you install a signal action in Haskell, you put a stable pointer to the action’s code into the array cell corresponding to the signal number, so that the timer thread could look it up later when an actual signal is delivered.
See also https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/Signals.
20150706T20:00:00Zhttp://roche.info/articles/20150706haskellsignals
It is widely agreed that the laws of the Applicative class are not pretty to look at.
pure id <*> v = v  identity
pure f <*> pure x = pure (f x)  homomorphism
u <*> pure y = pure ($ y) <*> u  interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)  composition
Monad laws, in comparison, not only look less odd to begin with but can also be stated in a much more elegant way in terms of Kleisli composition (<=<). Shouldn’t there be an analogous nice presentation for Applicative as well? That became a static question in my mind while I was studying applicative functors many moons ago. After finding surprisingly little commentary on this issue, I decided to try figuring it out by myself. 1
Let’s cast our eye over Applicative:
class Functor t => Applicative t where
pure :: a > t a
(<*>) :: t (a > b) > t a > t b
If our inspiration for reformulating Applicative is Kleisli composition, the only sensible plan is to look for a category in which the t (a > b) functionsinacontext from the type of (<*>) are the arrows, just like a > t b functions are arrows in a Kleisli category. Here is one way to state that plan in Haskell terms:
> class Applicative t => Starry t where
> idA :: t (a > a)
> (.*) :: t (b > c) > t (a > b) > t (a > c)
>
> infixl 4 .*
>  The Applicative constraint is wishful thinking:
>  When you wish upon a star...
The laws of Starry are the category laws for the t (a > b) arrows:
idA .* v = v  left identity
u .* idA = u  right identity
u .* v .* w = u .* (v .* w)  associativity
The question, then, is whether it is possible to reconstruct Applicative and its laws from Starry. The answer is a resounding yes! The proof is in this manuscript, which I have not transcribed here as it is a little too long for a leisurely post like this one 2. The argument is set in motion by establishing that pure is an arrow mapping from Hask to a Starry category, and that both (<*>) and (.*) are arrow mappings in the opposite direction. That leads to several naturality properties of those functors, from which the Applicative laws can be obtained. Along the way, we also get definitions for the Starry methods in terms of the Applicative ones…
> idA = pure id
> u .* v = fmap (.) u <*> v
… and viceversa:
pure x = fmap (const x) idA
u <*> v = fmap ($ ()) (u .* fmap const v)
Also interesting is how the property relating fmap and (<*>)…
fmap f u = pure f <*> u
… now tells us that a Functor is the result of composing the pure functor with the (<*>) functor. That becomes more transparent if we write it pointfree:
fmap = (<*>) . pure
In order to ensure Starry is equivalent to Applicative we still need to prove the converse, that is, obtain the Starry laws from the Applicative ones and the definitions of idA and (.*) just above. That is not difficult; all it takes is substituting the definitions in the Starry laws and:
For left identity, noticing that (id .) = id.
For right identity, applying the interchange law and noticing that ($ id) . (.) is id in a better disguise.
For associativity, using the laws to move all (.) to the left of the (<*>) and then verifying that the resulting messes of dots in both sides are equivalent.
As a tiny example, here is the Starry instance of Maybe…
instance Starry Maybe where
idA = Just id
Just g .* Just f = Just (g . f)
_ .* _ = Nothing
… and the verification of the laws for it:
 Left identity:
idA .* u = u
Just id .* u = u
 u = Nothing
Just id .* Nothing = Nothing
Nothing = Nothing
 u = Just f
Just id .* Just f = Just f
Just (id . f) = Just f
Just f = Just f
 Right identity:
u .* idA = u
u .* Just id = u
 u = Nothing
Nothing .* Just id = Nothing
Nothing = Nothing
 u = Just g
Just g .* Just id = Just g
Just (g .* id) = Just g
Just g = Just g
 Associativity:
u .* v .* w = u .* (v .* w)
 If any of u, v and w are Nothing, both sides will be Nothing.
Just h .* Just g .* Just f = Just h .* (Just g .* Just f)
Just (h . g) .* Just f = Just h .* (Just (g . f))
Just (h . g . f) = Just (h . (g . f))
Just (h . g . f) = Just (h . g . f)
It works just as intended:
GHCi> Just (2*) .* Just (subtract 3) .* Just (*4) <*> Just 5
Just 34
GHCi> Just (2*) .* Nothing .* Just (*4) <*> Just 5
Nothing
I do not think there will be many opportunities to use the Starry methods in practice. We are comfortable enough with applicative style, through which we see most t (a > b) arrows as intermediates generated on demand, rather than truly meaningful values. Furthermore, the Starry laws are not truly easier to prove (though they are certainly easier to remember!). Still, it was an interesting exercise to do, and it eases my mind to know that there is a neat presentation of the Applicative laws that I can relate to.
This post is Literate Haskell, in case you wish to play with Starry in GHCi (here is the raw .lhs file ).
> instance Starry Maybe where
> instance Starry [] where
> instance Starry ((>) a) where
> instance Starry IO where
As for proper implementations in libraries, the closest I found was Data.Semigroupoid.Static, which lives in Edward Kmett’s semigroupoids package. “Static arrows” is the actual technical term for the t (a > b) arrows. The module provides…
newtype Static f a b = Static { runStatic :: f (a > b) }
… which uses the definitions shown here for idA and (.*) as id and (.) of its Category instance.
There is a reasonably wellknown alternative formulation of Applicative: the Monoidal class as featured in this post by Edward Z. Yang. While the laws in this formulation are much easier to grasp, Monoidal feels a little alien from the perspective of a Haskeller, as it shifts the focus from function shuffling to tuple shuffling.↩
Please excuse some oddities in the manuscript, such as offkilter terminology and weird conventions (e.g. consistently naming arguments in applicative style as w <*> v <*> u rather than u <*> v <*> w in applicative style). The most baffling choice was using id rather than () as the throwaway argument to const. I guess I did that because ($ ()) looks bad in handwriting.↩
Comment on GitHub
(see the full post for a reddit link)
Post licensed under a
Creative Commons AttributionShareAlike 4.0 International License.
20150706T20:00:00Z
Daniel Mlot
Hi *,
Welcome for the latest entry in the GHC Weekly News. The past week, GHC HQ met up to discuss the status of the approaching 7.10.2 release.
7.10.2 status
After quite some delay due to a number of tricky regressions in 7.10.1, 7.10.2 is nearing the finish line. Austin cut release candidate 2 on Friday and so far the only reports of trouble appear to be some validation issues, most of which have already been fixed thanks to Richard Eisenberg.
7.10.2 will include a number of significant bugfixes. These include,
#10521, where overlap of floating point STG registers weren't properly accounted for, resulting in incorrect results in some floating point computations. This was fixed by the amazing Reid Barton.
#10534, a typesafety hole enabling a user to write unsafeCoerce with data families and coerce. Fix due to the remarkably Richard Eisenberg.
#10538, where some programs would cause the simplifier to emit an empty case, resulting in runtime crashes. Fix due to the industrious Simon Peyton Jones.
#10527, where the simplifier would expend a great deal of effort simplifying arguments which were never demanded by the callee.
#10414, where a subtle point of the runtime system's blackholing mechanism resulting in hangs on a carefully constructed testcase.
#10236, where incorrect DWARF annotations would be generated, resulting in incorrect backtraces. Fixed by Peter Wortmann
#7450, where cached free variable information was being unnecessarily dropped by the specialiser, resulting in nonlinear compile times for some programs.
See the status page for a complete listing of issues fixed in this release.
In the coming days we will being working with FP Complete to test the prerelease against Stackage. While Hackage tends to be too large to build in bulk, the selection of packages represented in Stackage is feasible to build and is likely to catch potential regressions. Hopefully this sort of largescale validation will become commonplace for future releases.
If all goes well, 7.10.2 will mark the end of the 7.10 series. However, there is always the small possibility that a major regression will be found. In this case we will cut a 7.10.3 release which will include a few patches which didn't make it into 7.10.2.
Other matters
It has been suggested in #10601 that GHC builds should ship with DWARF symbols for the base libraries and runtime system. While we all want to see this new capability in users' hands, 7.10.2 will, like 7.10.1, not be shipping with debug symbols. GHC HQ will be discussing the feasibility of including debug symbols with 7.12 in the future. In the meantime, we will be adding options to build.mk to make it easier for users to build their own compilers with debugenabled libraries.
In this week's GHC meeting the effort to port GHC's build system to the Shake? build system briefly came up. Despite the volume of updates on the Wiki Simon reports that the project is still moving along. The current state of the Shakebased build system can be found on Github.
While debugging #7540 it became clear that there may be trouble lurking in the profiler. Namely when profiling GHC itself lintAnnots is showing up strongly where it logically should not. This was previously addressed in #10007, which was closed after a patch by Simon Marlow was merged. As it appears that this did not fully resolve the issue I'll be looking further into this.
~ Ben
20150706T16:25:30Z
bgamari
NO UNTRACKED DEPENDENCIES!
Years ago, back when Isaac PotocznyJones and others were defining the
Cabal specification, the big idea was to make Haskell software portable
to different environments. One of the mantras was “no untracked
dependencies!”.
The problem at the time was that Haskell code [...]
The ChaCha cipher seems not to get as much love as Salsa20. Here is a stepbystep example of the ChaCha round function operating on a matrix. The format of the example is loosely based on the analogous example in section 4.1 of this Salsa20 paper: D. J. Bernstein. The Salsa20 family of stream ciphers. Document ID: 31364286077dcdff8e4509f9ff3139ad. URL: http://cr.yp.to/papers.html#salsafamily. Date: 2007.12.25.
original column [a;b;c;d]
61707865
04030201
14131211
00000007
after first line of round function
65737a66
04030201
14131211
7a616573
after second line of round function
65737a66
775858a7
8e747784
7a616573
after third line of round function
dccbd30d
775858a7
8e747784
aab67ea6
after all 4 lines of round function, i.e., quarter round
dccbd30d
395746a7
392af62a
aab67ea6
original matrix, with the same original column above
61707865 3320646e 79622d32 6b206574
04030201 08070605 0c0b0a09 100f0e0d
14131211 18171615 1c1b1a19 201f1e1d
00000007 00000000 01040103 06020905
one round (4 quarter rounds on columns)
dccbd30d 109b031b 0eb5ed20 4483ec2b
395746a7 d88a8f5f 7a292fab b06c9135
392af62a 6ac28db6 dfbce7ba a234a188
aab67ea6 e8383c7a 8d694938 0791063e
after shift rows
dccbd30d 109b031b 0eb5ed20 4483ec2b
d88a8f5f 7a292fab b06c9135 395746a7
dfbce7ba a234a188 392af62a 6ac28db6
0791063e aab67ea6 e8383c7a 8d694938
after another 4 quarter rounds on columns
06b44c34 69a94c11 2ce99b08 216830d1
29b215bd 721e2a33 f0a18097 708e1ee5
2b0e8de3 b801251f 42265fb2 696de1c2
e6fef362 c96c6325 c6cc126e 82c0635a
unshifting rows (concludes 1 double round)
06b44c34 69a94c11 2ce99b08 216830d1
708e1ee5 29b215bd 721e2a33 f0a18097
42265fb2 696de1c2 2b0e8de3 b801251f
c96c6325 c6cc126e 82c0635a e6fef362
after 8 rounds (4 double rounds)
f6093fbb efaf11c6 8bd2c9a4 bf1ff3da
bf543ce8 c46c6b5e c717fe59 863195b1
2775d1a0 babe2495 1b5c653e df7dc23c
5f3e08d7 041df75f f6e58623 abc0ab7e
Adding the original input to the output of 8 rounds
5779b820 22cf7634 0534f6d6 2a40594e
c3573ee9 cc737163 d3230862 9640a3be
3b88e3b1 d2d53aaa 37777f57 ff9ce059
5f3e08de 041df75f f7e98726 b1c2b483
reading the above as bytes, little endian
20 b8 79 57 34 76 cf 22 d6 f6 34 05 4e 59 40 2a
e9 3e 57 c3 63 71 73 cc 62 08 23 d3 be a3 40 96
b1 e3 88 3b aa 3a d5 d2 57 7f 77 37 59 e0 9c ff
de 08 3e 5f 5f f7 1d 04 26 87 e9 f7 83 b4 c2 b1
same as above but with 20000 rounds (10000 double rounds)
11 a3 0a d7 30 d2 a3 dc d8 ad c8 d4 b6 e6 63 32
72 c0 44 51 e2 4c ed 68 9d 8d ff 27 99 93 70 d4
30 2e 83 09 d8 41 70 49 2c 32 fd d9 38 cc c9 ae
27 97 53 88 ec 09 65 e4 88 ff 66 7e be 7e 5d 65
The example was calculated using an implementation of ChaCha in Haskell, whose end results agree with Bernstein's C reference implementation. The Haskell implementation is polymorphic, allowing as matrix elements any data type (of any word width) implementing Bits, and parametrizable to matrices of any size 4xN. (Security is probably bad for N not equal to 4. For word width different from 32, you probably want different rotation amounts.) The flexibility comes at a cost: the implemention is 3000 times slower than Bernstein's reference C implementation (which is in turn is slower than SIMD optimized assemblylanguage implementations).Also included in the same project is a similar Haskell implementation of Salsa20, parametrized to matrices of any size MxN because of the more regular structure of the Salsa20 quarter round function compared to ChaCha. We demonstrate taking advantage of polymorphism to use the same code both to evaluate Salsa20 on Word32 and to generate C code for the round function.
Announcing yesodtableOver the last two years, I've seen the need for safe dynamic tablebuilding
in half a dozen yesod projects I've worked on. After several design iterations,
the result of this experience is yesodtable,
which saw its first stable release last week. This blog post will contain code excerpts,
but you can also look at the documentation
the full example app on github,
which can be compiled and run.Naive SolutionBefore getting into specifics about yesodtable, I want to take a look at the naive
tablebuilding strategy and identify the common pitfalls. Let's say that you have a data
types Color and Person:data Color = Red  Green  Blue  Purple
deriving (Show)
data Person = Person
{ firstName :: Text
, lastName :: Text
, age :: Int
, favoriteColor :: Color
}We have a list of Person (let's call it people), and we want to show them all in a
table. You could write out a hamlet file like this:
First Name
Last Name
Age
$forall p < people
#{firstName p}
#{lastName p}
#{show (age p)}And there it is. This is the simplest solution to building a table. In fact, if you've worked
on web applications for any length of time, you've probably written code like this
before. I've implemented this pattern in PHP+html, in rails+haml, and in yesod+hamlet
projects. And every time, it is unsatisfactory.Problems With Naive SolutionLet's take a look at three reasons why this solution leaves us wanting something more:Duplication. After building a few tables this way, you realize that you are
copying the HTML elements and the list iteration ($forall) every time.Noncomposability. If I want to build a similar table, one that shows the
same fields but additionally has a column for favoriteColor, I have to copy
the whole thing. I can't glue another piece onto the end.Breakable Invariant. If we do decide to add a favoriteColor column, we might
try simply adding #{show (favoriteColor p)} to the end. This would cause incorrect
behavior at runtime, because we would have forgotten to add
Favorite Color to the table header. The problem is that we have an invariant
not captured by the type system: thead and the tbody loop must have the same
number of / elements, and the order must match.In particular, the last issue (breakable invariant) has been a source of great pains to me before.
On a threecolumn table, you are less likely to forget the or put it in the wrong place.
As the table gets larger though (six or more columns), these mistakes become easier to make, and it's
harder to be sure that you did the right thing until you see it at runtime.Example with yesodtableSo let's take a look at how yesodtable addresses these issues. The module it provides
should be imported as follows:import Yesod.Table (Table)
import qualified Yesod.Table as TableLet's build the same table we saw earlier:peopleBasicInfoTable :: Table site Person
peopleBasicInfoTable = mempty
<> Table.text "First Name" firstName
<> Table.text "Last Name" lastName
<> Table.string "Age" (show . age)And then we can feed it data and render it with buildBootstrap: Although it's called buildBootstrap, it builds a table just fine
 if you aren't using bootstrap. It just adds bootstrap's table classes.
getExamplePeopleR = defaultLayout $ Table.buildBootstrap peopleTable peopleExplanation of InternalsThe key to this approach is looking at a table pattern (called a Table in this library)
as a collection of columns, not a collection of rows. From the yesodtable source, we have:newtype Table site a = Table (Seq (Column site a))
deriving (Monoid)
data Column site a = Column
{ header :: !(WidgetT site IO ())
, cell :: !(a > WidgetT site IO ())
}Each column is just the content that will go in the (the value of header) and
a function that, given the data for a table row, will produce the content that belongs
in the . A table is trivially a collection of columns and gets a Monoid
instance from Seq for free (for those unfamiliar, Seq a is like [a] but with
different performance characteristics). Consequently, any two Tables that are
parameterized over the same types can be concatenated. As a final note of explanation,
the Table.text function that we saw above just a helper for building singleton
tables. So, the three Tables below are equivalant:import qualified Data.Sequence as Seq
import qualified Data.Text as Text
 These three generate a singlecolumn table that displays the age.
reallyEasyToReadTable, easyToReadTable, hardToReadTable :: Table site Person
reallyEasyToReadTable = Table.int "Age" age
easyToReadTable = Table.text "Age" (Text.pack . show . age)
hardToReadTable = Table.Table $ Seq.singleton $ Table.Column
(toWidget $ toHtml "Age")
(toWidget . toHtml . show . age)As should be clear, the convenience functions for singleton Tables should always be
preferred.How Is This Better?Now to address the most important question: Why is this better than what we had earlier?
Firstly, consider the issue of the breakable invariant. This is now a nonissue. Imagine
that we modified the earlier table to show a person's favorite color as well:peopleFullInfoTable1 :: Table site Person
peopleFullInfoTable1 = mempty
<> Table.text "First Name" firstName
<> Table.text "Last Name" lastName
<> Table.text "Age" (show . age)
<> Table.string "Favorite Color" (show . favoriteColor)The table is correct by construction. You cannot forget the column header because
it's part of the Column data type. You're less likely to make this mistake, because
now that information is directly beside the contentextracting function, but even
if you somehow typed this instead, you would get a compiletime error: <> Table.string (show . favoriteColor)Secondly, we can look at duplication. All the
tablerendering logic is moved into buildBootstrap (and you can write your own
table renderer if that one is not satisfactory). The Table that we are using now
has neither the HTML elements nor the list iteration that we dealt with earlier.Finally, we can look at composability. As an alternative way of adding the column
for a person's favorite color, we could write:peopleFullInfoTable2 :: Table site Person
peopleFullInfoTable2 = mempty
<> peopleBasicInfoTable
<> Table.string "Favorite Color" (show . favoriteColor)Additionally, if we need to promote this Table to work on something
like Entity Person (if it was backed by persistent), we could do this: You need to use ekmett's contravariant package
peopleEntityFullInfoTable :: Table site (Entity Person)
peopleEntityFullInfoTable = contramap entityVal peopleFullInfoTable2I won't go into contravariant functors here, but it's a very useful pattern
for working with Tables. The astute reader will notice
that the monoidal composition pattern shown earlier means that we can only append
or prepend columns. We cannot inject them into the middle. I'll give
yesodtable a B minus on to composability objective.Closing Notes and AcknowledgementsOne final closing note. You may have noticed that all of the Tables in this
post were parameterized over site. This is because they don't depend on
a particular foundation type. Usually, the way that this can happen is that
you use a route in one of the columns: Assume that our foundation type was named App
peopleTableWithLink :: Table App (Entity Person)
peopleTableWithLink = mempty
<> peopleEntityFullInfoTable
<> Table.linked "Profile Page" (const "View") (PersonProfileR . entityKey)The above example must be parameterized over App (or whatever your foundation
type is named), not over site.This monoidal approach to building tables was inspired by Gabriel Gonzalez's
Equational Reasoning at Scale
and by the classic diagrams paper.
I hope that others find the library useful. I am very open to pull requests and suggestions, so if
you have an idea for a convenience function, feel free to open up an issue on
the github page.
Posted on July 6, 2015
Tags: jonprl, types
I was just over at OPLSS for the last two weeks. While there I finally met Jon Sterling in person. What was particularly fun is that for that last few months he’s been creating a proof assistant called JonPRL in the spirit of Nuprl. As it turns out, it’s quite a fun project to work on so I’ve implemented a few features in it over the last couple of days and learned more or less how it works.
Since there’s basically no documentation on it besides the readme and of course the compiler so I thought I’d write down some of the stuff I’ve learned. There’s also a completely separate post on the underlying type theory for Nuprl and JonPRL that’s very interesting in its own right but this isn’t it. Hopefully I’ll get around to scribbling something about that because it’s really quite clever.
Here’s the layout of this tutorial
First we start with a whirlwind tutorial. I’ll introduce the basic syntax and we’ll go through some simple proofs together
I’ll then dive into some of the rational behind JonPRL’s theory. This should help you understand why some things work how they do
I’ll show off a few of JonPRL’s more unique features and (hopefully) interest you enough to start fiddling on your own
Getting JonPRL
JonPRL is pretty easy to build and install and having it will make this post more enjoyable. You’ll need smlnj since JonPRL is currently written in SML. This is available in most package managers (including homebrew) otherwise just grab the binary from the website. After this the following commands should get you a working executable
git clone ssh://git@github.com/jonsterling/jonprl
cd jonprl
git submodule init
git submodule update
make (This is excitingly fast to run)
make test (If you’re doubtful)
You should now have an executable called jonprl in the bin folder. There’s no prelude for jonprl so that’s it. You can now just feed it files like any reasonable compiler and watch it spew (currently difficulttodecipher) output at you.
If you’re interested in actually writing JonPRL code, you should probably install David Christiansen’s Emacs mode. Now that we’re up and running, let’s actually figure out how the language works
The Different Languages in JonPRL
JonPRL is composed of really 3 different sorts of minilanguages
The term language
The tactic language
The language of commands to the proof assistant
In Coq, these roughly correspond to Gallina, Ltac, and Vernacular respectively.
The Term Language
The term language is an untyped language that contains a number of constructs that should be familiar to people who have been exposed to dependent types before. The actual concrete syntax is composed of 3 basic forms:
We can apply an “operator” (I’ll clarify this in a moment) with op(arg1; arg2; arg3).
We have variables with x.
And we have abstraction with x.e. JonPRL has one construct for binding x.e built into its syntax, that things like λ or Π are built off of.
An operator in this context is really anything you can imagine having a node in an AST for a language. So something like λ is an operator, as is if or pair (corresponding to (,) in Haskell). Each operator has a piece of information associated with it, called its arity. This arity tells you how many arguments an operator takes and how many variables x.y.z. ... each is allowed to bind. For example, with λ has an arity is written (1) since it takes 1 argument which binds 1 variable. Application (ap) has the arity (0; 0). It takes 2 arguments neither of which bind a variable.
So as mentioned we have functions and application. This means we could write (λx.x) y in JonPRL as ap(λ(x.x); y). The type of functions is written with Π. Remember that JonPRL’s language has a notion of dependence so the arity is (0; 1). The construct Π(A; x.B) corresponds to (x : A) → B in Agda or forall (x : A), B in Coq.
We also have dependent sums as well (Σs). In Agda you would write (M , N) to introduce a pair and Σ A λ x → B to type it. In JonPRL you have pair(M; N) and Σ(A; x.B). To inspect a Σ we have spread which let’s us eliminate a pair pair. Eg spread(0; 2) and you give it a Σ in the first spot and x.y.e in the second. It’ll then replace x with the first component and y with the second. Can you think of how to write fst and snd with this?
There’s sums, so inl(M), inr(N) and +(A; B) corresponds to Left, Right, and Either in Haskell. For case analysis there’s decide which has the arity (0; 1; 1). You should read decide(M; x.N; y.P) as something like
case E of
Left x > L
Right y > R
In addition we have unit and <> (pronounced axe for axiom usually). Neither of these takes any arguments so we write them just as I have above. They correspond to Haskell’s type and valuelevel () respectively. Finally there’s void which is sometimes called false or empty in theorem prover land.
You’ll notice that I presented a bunch of types as if they were normal terms in this section. That’s because in this untyped computation system, types are literally just terms. There’s no typing relation to distinguish them yet so they just float around exactly as if they were λ or something! I call them types because I’m thinking of later when we have a typing relation built on top of this system but for now there are really just terms. It was still a little confusing for me to see Π(unit; _.unit) in a language without types, so I wanted to make this explicit.
Now we can introduce some more exotic terms. Later, we’re going to construct some rules around them that are going to make it behave that way we might expect but for now, they are just suggestively named constants.
U{i}, the ith level universe used to classify all types that can be built using types other than U{i} or higher. It’s closed under terms like Π and it contains all the types of smaller universes
=(0; 0; 0) this is equality between two terms at a type. It’s a proposition that’s going to precisely mirror what’s going on later in the type theory with the equality judgment
∈(0; 0) this is just like = but internalizes membership in a type into the system. Remember that normally “This has that type” is a judgment but with this term we’re going to have a propositional counterpart to use in theorems.
In particular it’s important to distinguish the difference between ∈ the judgment and ∈ the term. There’s nothing inherent in ∈ above that makes it behave like a typing relation as you might expect. It’s on equal footing with flibbertyjibberty(0; 0; 0).
This term language contains the full untyped lambda calculus so we can write all sorts of fun programs like
λ(f.ap(λ(x.ap(f;(ap(x;x)))); λ(x.ap(f;(ap(x;x)))))
which is just the Y combinator. In particular this means that there’s no reason that every term in this language should normalize to a value. There are plenty of terms in here that diverge and in principle, there’s nothing that rules out them doing even stranger things than that. We really only depend on them being deterministic, that e ⇒ v and e ⇒ v' implies that v = v'.
Tactics
The other big language in JonPRL is the language of tactics. Luckily, this is very familiarly territory if you’re a Coq user. Unluckily, if you’ve never heard of Coq’s tactic mechanism this will seem completely alien. As a quick high level idea for what tactics are:
When we’re proving something in a proof assistant we have to deal with a lot of boring mechanical details. For example, when proving A → B → A I have to describe that I want to introduce the A and the B into my context, then I have to suggest using that A the context as a solution to the goal. Bleh. All of that is pretty obvious so let’s just get the computer to do it! In fact, we can build up a DSL of composable “proof procedures” or /tactics/ to modify a particular goal we’re trying to prove so that we don’t have to think so much about the low level details of the proof being generated. In the end this DSL will generate a proof term (or derivation in JonPRL) and we’ll check that so we never have to trust the actual tactics to be sound.
In Coq this is used to great effect. In particular see Adam Chlipala’s book to see incredibly complex theorems with oneline proofs thanks to tactics.
In JonPRL the tactic system works by modifying a sequent of the form H ⊢ A (a goal). Each time we run a tactic we get back a list of new goals to prove until eventually we get to trivial goals which produce no new subgoals. This means that when trying to prove a theorem in the tactic language we never actually see the resulting evidence generated by our proof. We just see this list of H ⊢ As to prove and we do so with tactics.
The tactic system is quite simple, to start we have a number of basic tactics which are useful no matter what goal you’re attempting to prove
id a tactic which does nothing
t1; t2 this runs the t1 tactic and runs t2 on any resulting subgoals
*{t} this runs t as long as t does something to the goal. If t ever fails for whatever reason it merely stops running, it doesn’t fail itself
?{t} tries to run t once. If t fails nothing happens
!{t} runs t and if t does anything besides complete the proof it fails. This means that !{id} for example will always fail.
t1  t2 runs t1 and if it fails it runs t2. Only one of the effects for t1 and t2 will be shown.
t; [t1, ..., tn] first runs t and then runs tactic ti on subgoal ith subgoal generated by t
trace "some words" will print some words to standard out. This is useful when trying to figure out why things haven’t gone your way.
fail is the opposite of id, it just fails. This is actually quite useful for forcing backtracking and one could probably implement a makeshift !{} as t; fail.
It’s helpful to see this as a sort of tree, a tactic takes one goal to a list of a subgoals to prove so we can imagine t as this part of a tree
H

———–————————— (t)
H' H'' H'''
If we have some tactic t2 then t; t2 will run t and then run t2 on H, H', and H''. Instead we could have t; [t1, t2, t3] then we’ll run t and (assuming it succeeds) we’ll run t1 on H', t2 on H'', and t3 on H'''. This is actually how things work under the hood, composable fragments of trees :)
Now those give us a sort of bedrock for building up scripts of tactics. We also have a bunch of tactics that actually let us manipulate things we’re trying to prove. The 4 big ones to be aware of are
intro
elim #NUM
eqcd
memcd
The basic idea is that intro modifies the A part of the goal. If we’re looking at a function, so something like H ⊢ Π(A; x.B), this will move that A into the context, leaving us with H, x : A ⊢ B.
If you’re familiar with sequent calculus intro runs the appropriate right rule for the goal. If you’re not familiar with sequent calculus intro looks at the outermost operator of the A and runs a rule that applies when that operator is to the right of a the ⊢.
Now one tricky case is what should intro do if you’re looking at a Σ? Well now things get a bit dicey. We’d might expect to get two subgoals if we run intro on H ⊢ Σ(A; x.B), one which proves H ⊢ A and one which proves H ⊢ B or something, but what about the fact that x.B depends on whatever the underlying realizer (that’s the program extracted from) the proof of H ⊢ A! Further, Nuprl and JonPRL are based around extractstyle proof systems. These mean that a goal shouldn’t depend on the particular piece of evidence proving of another goal. So instead we have to tell intro up front what we want the evidence for H ⊢ A to be is so that the H ⊢ B section may use it.
To do this we just give intro an argument. For example say we’re proving that · ⊢ Σ(unit; x.unit), we run intro [<>] which gives us two subgoals · ⊢ ∈(<>; unit) and · ⊢ unit. Here the [] let us denote the realizer we’re passing to intro. In general any term arguments to a tactic will be wrapped in []s. So the first goal says “OK, you said that this was your realizer for unit, but is it actually a realizer for unit?” and the second goal substitutes the given realizer into the second argument of Σ, x.unit, and asks us to prove that. Notice how here we have to prove ∈(<>; unit)? This is where that weird ∈ type comes in handy. It let’s us sort of play type checker and guide JonPRL through the process of type checking. This is actually very crucial since type checking in Nuprl and JonPRL is undecidable.
Now how do we actually go about proving ∈(<>; unit)? Well here memcd has got our back. This tactic transforms ∈(A; B) into the equivalent form =(A; A; B). In JonPRL and Nuprl, types are given meaning by how we interpret the equality of their members. In other words, if you give me a type you have to say
What canonical terms are in that terms
What it means for two canonical members to be equal
Long ago, Stuart Allen realized we could combine the two by specifying a partial equivalence relation for a type. In this case rather than having a separate notion of membership we check to see if something is equal to itself under the PER because when it is that PER behaves like a normal equivalence relation! So in JonPRL ∈ is actually just a very thin layer of sugar around = which is really the core defining notion of typehood. To handle = we have eqcd which does clever things to handle most of the obvious cases of equality.
Finally, we have elim. Just like intro let us simplify things on the right of the ⊢, elim let’s us eliminate something on the left. So we tell elim to “eliminate” the nth item in the context (they’re numbered when JonPRL prints them) with elim #n.
Just like with anything, it’s hard to learn all the tactics without experimenting (though a complete list can be found with jonprl listtactics). Let’s go look at the command language so we can actually prove some theorems.
Commands
So in JonPRL there are only 4 commands you can write at the top level
Operator
[oper] =def= [term] (A definition)
Tactic
Theorem
The first three of these let us customize and extend the basic suite of operators and tactics JonPRL comes with. The last actually lets us state and prove theorems.
The best way to see these things is by example so we’re going to build up a small development in JonPRL. We’re going to show that products are monoid with unit up to some logical equivalence. There are a lot of proofs involved here
prod(unit; A) entails A
prod(A; unit) entails A
A entails prod(unit; A)
A entails prod(A; unit)
prod(A; prod(B; C)) entails prod(prod(A; B); C)
prod(prod(A; B); C) entails prod(A; prod(B; C))
I intend to prove 1, 2, and 5. The remaining proofs are either very similar or fun puzzles to work on. We could also prove that all the appropriate entailments are inverses and then we could say that everything is up to isomorphism.
First we want a new snazzy operator to signify nondependent products since writing Σ(A; x.B) is kind of annoying. We do this using operator
Operator prod : (0; 0).
This line declares prod as a new operator which takes two arguments binding zero variables each. Now we really want JonPRL to know that prod is sugar for Σ. To do this we use =def= which gives us a way to desugar a new operator into a mess of existing ones.
[prod(A; B)] =def= [Σ(A; _.B)].
Now we can change any occurrence of prod(A; B) for Σ(A; _.B) as we’d like. Okay, so we want to prove that we have a monoid here. What’s the first step? Let’s verify that unit is a left identity for prod. This entails proving that for all types A, prod(unit; A) ⊃ A and A ⊃ prod(unit; A). Let’s prove these as separate theorems. Translating our first statement into JonPRL we want to prove
Π(U{i}; A.
Π(prod(unit; A); _.
A))
In Agda notation this would be written
(A : Set) → (_ : prod(unit; A)) → A
Let’s prove our first theorem, we start by writing
Theorem leftid1 :
[Π(U{i}; A.
Π(prod(unit; A); _.
A))] {
id
}.
This is the basic form of a theorem in JonPRL, a name, a term to prove, and a tactic script. Here we have id as a tactic script, which clearly doesn’t prove our goal. When we run JonPRL on this file (Cc Cl if you’re in Emacs) you get back
[XXX.jonprl:8.39.1]: tactic 'COMPLETE' failed with goal:
⊢ ΠA ∈ U{i}. (prod(unit; A)) => A
Remaining subgoals:
⊢ ΠA ∈ U{i}. (prod(unit; A)) => A
So focus on that Remaining subgoals bit, that’s what we have left to prove, it’s our current goal. Now you may notice that this outputted goal is a lot prettier than our syntax! That’s because currently in JonPRL the input and outputted terms may not match, the latter is subject to pretty printing. In general this is great because you can read your remaining goals, but it does mean copying and pasting is a bother. There’s nothing to the left of that ⊢ yet so let’s run the only applicable tactic we know. Delete that id and replace it with
{
intro
}.
The goal now becomes
Remaining subgoals:
1. A : U{i}
⊢ (prod(unit; A)) => A
⊢ U{i} ∈ U{i'}
Two ⊢s means two subgoals now. One looks pretty obvious, U{i'} is just the universe above U{i} (so that’s like Set₁ in Agda) so it should be the case that U{i} ∈ U{i'} by definition! So the next tactic should be something like [???, memcd; eqcd]. Now what should that ??? be? Well we can’t use elim because there’s one thing in the context now (A : U{i}), but it doesn’t help us really. Instead let’s run unfold . This is a new tactic that’s going to replace that prod with the definition that we wrote earlier.
{
intro; [unfold , memcd; eqcd]
}
Notice here that , behinds less tightly than ; which is useful for saying stuff like this. This gives us
Remaining subgoals:
1. A : U{i}
⊢ (unit × A) => A
We run intro again
{
intro; [unfold , memcd; eqcd]; intro
}
Now we are in a similar position to before with two subgoals.
Remaining subgoals:
1. A : U{i}
2. _ : unit × A
⊢ A
1. A : U{i}
⊢ unit × A ∈ U{i}
The first subgoal is really what we want to be proving so let’s put a pin in that momentarily. Let’s get rid of that second subgoal with a new helpful tactic called auto. It runs eqcd, memcd and intro repeatedly and is built to take care of boring goals just like this!
{
intro; [unfold , memcd; eqcd]; intro; [id, auto]
}
Notice that we used what is a pretty common pattern in JonPRL, to work on one subgoal at a time we use []’s and ids everywhere except where we want to do work, in this case the second subgoal.
Now we have
Remaining subgoals:
1. A : U{i}
2. _ : unit × A
⊢ A
Cool! Having a pair of unit × A really ought to mean that we have an A so we can use elim to get access to it.
{
intro; [unfold , memcd; eqcd]; intro; [id, auto];
elim #2
}
This gives us
Remaining subgoals:
1. A : U{i}
2. _ : unit × A
3. s : unit
4. t : A
⊢ A
We’ve really got the answer now, #4 is precisely our goal. For this situations there’s assumption which is just a tactic which succeeds if what we’re trying to prove is in our context already. This will complete our proof
Theorem leftid1 :
[Π(U{i}; A.
Π(prod(unit; A); _.
A))] {
intro; [unfold , memcd; eqcd]; intro; [id, auto];
elim #2; assumption
}.
Now we know that auto will run all of the tactics on the first line except unfold , so what we just unfold first and run auto? It ought to do all the same stuff.. Indeed we can shorten our whole proof to unfold ; auto; elim #2; assumption. With this more heavily automated proof, proving our next theorem follows easily.
Theorem rightid1 :
[Π(U{i}; A.
Π(prod(A; unit); _.
A))] {
unfold ; auto; elim #2; assumption
}.
Next, we have to prove associativity to complete the development that prod is a monoid. The statement here is a bit more complex.
Theorem assoc :
[Π(U{i}; A.
Π(U{i}; B.
Π(U{i}; C.
Π(prod(A; prod(B;C)); _.
prod(prod(A;B); C)))))] {
id
}.
In Agda notation what I’ve written above is
assoc : (A B C : Set) → A × (B × C) → (A × B) × C
assoc = ?
Let’s kick things off with unfold ; auto to deal with all the boring stuff we had last time. In fact, since x appears in several nested places we’d have to run unfold quite a few times. Let’s just shorten all of those invocations into *{unfold }
{
*{unfold }; auto
}
This leaves us with the state
Remaining subgoals:
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ A
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ B
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ C
In each of those goals we need to take apart the 4th hypothesis so let’s do that
{
*{unfold }; auto; elim #4
}
This leaves us with 3 subgoals still
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ A
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ B
1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ C
The first subgoal is pretty easy, assumption should handle that. In the other two we want to eliminate 6 and then we should be able to apply assumption. In order to deal with this we use  to encode that disjunction. In particular we want to run assumption OR elim #6; assumption leaving us with
{
*{unfold }; auto; elim #4; (assumption  elim #6; assumption)
}
This completes the proof!
Theorem assoc :
[Π(U{i}; A.
Π(U{i}; B.
Π(U{i}; C.
Π(prod(A; prod(B;C)); _.
prod(prod(A;B); C)))))] {
*{unfold }; auto; elim #4; (assumption  elim #6; assumption)
}.
As a fun puzzle, what needs to change in this proof to prove we can associate the other way?
What on earth did we just do!?
So we just proved a theorem.. but what really just happened? I mean how did we go from “Here we have an untyped computation system which types just behaving as normal terms” to “Now apply auto and we’re done!”. In this section I’d like to briefly sketch the path from untyped computation to theorems.
The path looks like this
We start with our untyped language and its notion of computation
We already discussed this in great depth before.
We define a judgment a = b ∈ A.
This is a judgment, not a term in that language. It exists in whatever metalanguage we’re using. This judgment is defined across 3 terms in our untyped language (I’m only capitalizing A out of convention). This is supposed to represent that a and b are equal elements of type A. This also gives meaning to typehood: something is a type in CTT precisely when we know what the partial equivalence relation defined by  =  ∈ A on canonical values is.
Notice here that I said partial. It isn’t the case that a = b ∈ A presupposes that we know that a : A and b : A because we don’t have a notion of : yet!
In some sense this is where we depart from a type theory like Coq or Agda’s. We have programs already and on top of them we define this 3 part judgment which interacts which computation in a few ways I’m not specifying. In Coq, we would specify one notion of equality, generic over all types, and separately specify a typing relation.
From here we can define the normal judgments of Martin Lof’s type theory. For example, a : A is a = a ∈ A. We recover the judgment A type with A = A ∈ U (where U here is a universe).
This means that inhabiting a universe A = A ∈ U, isn’t necessarily inductively defined but rather negatively generated. We specify some condition a term must satisfy to occupy a universe.
Hypothetical judgments are introduced in the same way they would be in MartinLof’s presentations of type theory. The idea being that H ⊢ J if J is evident under the assumption that each term in H has the appropriate type and furthermore that J is functional (respects equality) with respect to what H contains. This isn’t really a higher order judgment, but it will be defined in terms of a higher order hypothetical judgment in the metatheory.
With this we have something that walks and quacks like normal type theory. Using the normal tools of our metatheory we can formulate proofs of a : A and do normal type theory things. This whole development is building up what is called “Computational Type Theory”. The way this diverges from MartinLof’s extensional type theory is subtle but it does directly descend from MartinLof’s famous 1979 paper “Constructive Mathematics and Computer Programming” (which you should read. Instead of my blog post).
Now there’s one final layer we have to consider, the PRL bit of JonPRL. We define a new judgment, H ⊢ A [ext a]. This is judgment is cleverly set up so two properties hold
H ⊢ A [ext a] should entail that H ⊢ a : A or H ⊢ a = a ∈ A
In H ⊢ A [ext a], a is an output and H and A are inputs. In particular, this implies that in any inference for this judgment, the subgoals may not use a in their H and A.
This means that a is completely determined by H and A which justifies my use of the term output. I mean this in the sense of Twelf and logic programming if that’s a more familiar phrasing. It’s this judgment that we see in JonPRL! Since that a is output we simply hide it, leaving us with H ⊢ A as we saw before. When we prove something with tactics in JonPRL we’re generating a derivation, a tree of inference rules which make H ⊢ A evident for our particular H and A! These rules aren’t really programs though, they don’t correspond one to one with proof terms we may run like they would in Coq. The computational interpretation of our program is bundled up in that a.
To see what I mean here we need a little bit more machinery. Specifically, let’s look at the rules for the equality around the proposition =(a; b; A). Remember that we have a term <> lying around,
a = b ∈ A
————————————————————
<> = <> ∈ =(a; b; A)
So the only member of =(a; b; A) is <> if a = b ∈ A actually holds. First off, notice that <> : A and <> : B doesn’t imply that A = B! In another example, λ(x. x) ∈ Π(A; _.A) for all A! This is a natural consequence of separating our typing judgment from our programming language. Secondly, there’s not really any computation in the e of H ⊢ =(a; b; A) (e). After all, in the end the only thing e could be so that e : =(a; b; A) is <>! However, there is potentially quite a large derivation involved in showing =(a; b; A)! For example, we might have something like this
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption
Now we write derivations of this sequent up side down, so the thing we want to show starts on top and we write each rule application and subgoal below it (AI people apparently like this?). Now this was quite a derivation, but if we fill in the missing [ext e] for this derivation from the bottom up we get this
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption [ext x]
Notice how at the bottom there was some computational content (That x signifies that we’re accessing a variable in our context) but than we throw it away right on the next line! That’s because we find that no matter what the extract was that let’s us derive =(b; a; A), the only realizer it could possible generate is <>. Remember our conditions, if we can make evident the fact that b = a ∈ A then <> ∈ =(b; a; A). Because we somehow managed to prove that b = a ∈ A holds, we’re entitled to just use <> to realize our proof. This means that despite our somewhat tedious derivation and the bookkeeping that we had to do to generate that program, that program reflects none of it.
This is why type checking in JonPRL is woefully undecidable: in part, the realizers that we want to type check contain none of the helpful hints that proof terms in Coq would. This also means that extraction from JonPRL proofs is built right into the system and we can actually generate cool and useful things! In Nuprlland, folks at Cornell actually write proofs and use this realizers to run real software. From what Bob Constable said at OPLSS they can actually get these programs to run fast (within 5x of naive C code).
So to recap, in JonPRL we
See H ⊢ A
Use tactics to generate a derivation of this judgment
Once this derivation is generated, we can extract the computational content as a program in our untyped system
In fact, we can see all of this happen if you call JonPRL from the command line or hit Cc Cc in emacs! On our earlier proof we see
Operator prod : (0; 0).
⸤prod(A; B)⸥ ≝ ⸤A × B⸥.
Theorem leftid1 : ⸤⊢ ΠA ∈ U{i}. (prod(unit; A)) => A⸥ {
funintro(A.funintro(_.prodelim(_; _.t.t); prod⁼(unit⁼; _.hyp⁼(A))); U⁼{i})
} ext {
λ_. λ_. spread(_; _.t.t)
}.
Theorem rightid1 : ⸤⊢ ΠA ∈ U{i}. (prod(A; unit)) => A⸥ {
funintro(A.funintro(_.prodelim(_; s._.s); prod⁼(hyp⁼(A); _.unit⁼)); U⁼{i})
} ext {
λ_. λ_. spread(_; s._.s)
}.
Theorem assoc : ⸤⊢ ΠA ∈ U{i}. ΠB ∈ U{i}. ΠC ∈ U{i}. (prod(A; prod(B; C))) => prod(prod(A; B); C)⸥ {
funintro(A.funintro(B.funintro(C.funintro(_.independentprodintro(independentprodintro(prodelim(_;
s.t.prodelim(t; _._.s)); prodelim(_; _.t.prodelim(t;
s'._.s'))); prodelim(_; _.t.prodelim(t; _.t'.t')));
prod⁼(hyp⁼(A); _.prod⁼(hyp⁼(B); _.hyp⁼(C)))); U⁼{i}); U⁼{i});
U⁼{i})
} ext {
λ_. λ_. λ_. λ_. ⟨⟨spread(_; s.t.spread(t; _._.s)), spread(_; _.t.spread(t; s'._.s'))⟩, spread(_; _.t.spread(t; _.t'.t'))⟩
}.
Now we can see that those Operator and ≝ bits are really what we typed with =def= and Operator in JonPRL, what’s interesting here are the theorems. There’s two bits, the derivation and the extract or realizer.
{
derivation of the sequent · ⊢ A
} ext {
the program in the untyped system extracted from our derivation
}
We can move that derivation into a different proof assistant and check it. This gives us all the information we need to check that JonPRL’s reasoning and helps us not trust all of JonPRL (I wrote some of it so I’d be a little scared to trust it :). We can also see the computational bit of our proof in the extract. For example, the computation involved in taking A × unit → A is just λ_. λ_. spread(_; s._.s)! This is probably closer to what you’ve seen in Coq or Idris, even though I’d say the derivation is probably more similar in spirit (just ugly and beta normal). That’s because the extract need not have any notion of typing or proof, it’s just the computation needed to produce a witness of the appropriate type. This means for a really tricky proof of equality, your extract might just be <>! Your derivation however will always exactly reflect the complexity of your proof.
Killer features
OK, so I’ve just dumped about 50 years worth of hard research in type theory into your lap which is best left to ruminate for a bit. However, before I finish up this post I wanted to do a little bit of marketing so that you can see why one might be interested in JonPRL (or Nuprl). Since we’ve embraced this idea of programs first and types as PERs, we can define some really strange types completely seamlessly. For example, in JonPRL there’s a type ⋂(A; x.B), it behaves a lot like Π but with one big difference, the definition of  =  ∈ ⋂(A; x.B) looks like this
a : A ⊢ e = e' ∈ [a/x]B
————————————————————————
e = e' ∈ ⋂(A; x.B)
Notice here that e and e' may not use a anywhere in their bodies. That is, they have to be in [a/x]B without knowing anything about a and without even having access to it.
This is a pretty alien concept that turned out to be new in logic as well (it’s called “uniform quantification” I believe). It turns out to be very useful in PRL’s because it lets us declare things in our theorems without having them propogate into our witness. For example, we could have said
Theorem rightid1 :
[⋂(U{i}; A.
Π(prod(A; unit); _.
A))] {
unfold ; auto; elim #2; assumption
}.
With the observation that our realizer doesn’t need to depend on A at all (remember, no types!). Then the extract of this theorem is
λx. spread(x; s._.s)
There’s no spurious λ _. ... at the beginning! Even more wackily, we can define subsets of an existing type since realizers need not have unique types
e = e' ∈ A [e/x]P [e'/x]P
————————————————————————————
e = e' ∈ subset(A; x.P)
And in JonPRL we can now say things like “all odd numbers” by just saying subset(nat; n. ap(odd; n)). In intensional type theories, these types are hard to deal with and still the subject of open research. In CTT they just kinda fall out because of how we thought about types in the first place. Quotients are a similarly natural conception (just define a new type with a stricter PER) but JonPRL currently lacks them (though they shouldn’t be hard to add..).
Finally, if you’re looking for one last reason to dig into **PRL, the fact that we’ve defined all our equalities extensionally means that several very useful facts just fall right out of our theory
Theorem funext :
[⋂(U{i}; A.
⋂(Π(A; _.U{i}); B.
⋂(Π(A; a.ap(B;a)); f.
⋂(Π(A; a.ap(B;a)); g.
⋂(Π(A; a.=(ap(f; a); ap(g; a); ap(B; a))); _.
=(f; g; Π(A; a.ap(B;a))))))))] {
auto; ext; ?{elim #5 [a]}; auto
}.
This means that two functions are equal in JonPRL if and only if they map equal arguments to equal output. This is quite pleasant for formalizing mathematics for example.
Wrap Up
Whew, we went through a lot! I didn’t intend for this to be a full tour of JonPRL, just a taste of how things sort of hang together and maybe enough to get you looking through the examples. Speaking of which, JonPRL comes with quite a few examples which are going to make a lot more sense now.
Additionally, you may be interested in the documentation in the README which covers most of the primitive operators in JonPRL. As for an exhaustive list of tactics, well….
Hopefully I’ll be writing about JonPRL again soon. Until then, I hope you’ve learned something cool :)
A huge thanks to David Christiansen and Jon Sterling for tons of helpful feedback on this
var disqus_shortname = 'codeco';
(function() {
var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
(document.getElementsByTagName('head')[0]  document.getElementsByTagName('body')[0]).appendChild(dsq);
})();
Please enable JavaScript to view the comments powered by Disqus.
comments powered by Disqus
20150706T00:00:00Z
I’ve just submitted a new draft, Crossplatform Compilers for Functional Languages. Abstract: Modern software is often designed to run on a virtual machine, such as the JVM or .NET’s CLR. Increasingly, even the web browser is considered a target platform with the Javascript engine as its virtual machine. The choice of programming language for a […]
I just started implementing SipHash in
hashabler and wanted to share
a nice way I found to translate stateful bittwiddling code in C (which makes
heavy use of bitwise assignment operators) to haskell.
I was working from the
reference implementation.
As you can see statefulness and mutability are an implicit part of how the
algorithm is defined, as it modifies the states of the v variables.
#define SIPROUND \
do { \
v0 += v1; v1=ROTL(v1,13); v1 ^= v0; v0=ROTL(v0,32); \
v2 += v3; v3=ROTL(v3,16); v3 ^= v2; \
v0 += v3; v3=ROTL(v3,21); v3 ^= v0; \
v2 += v1; v1=ROTL(v1,17); v1 ^= v2; v2=ROTL(v2,32); \
} while(0)
int siphash( uint8_t *out, const uint8_t *in, uint64_t inlen, const uint8_t *k )
{
/* ... */
for ( ; in != end; in += 8 )
{
m = U8TO64_LE( in );
v3 ^= m;
TRACE;
for( i=0; i SipKey > a > Word64
siphash (k0,k1) = \a> runIdentity $ do
let v0 = 0x736f6d6570736575
v1 = 0x646f72616e646f6d
v2 = 0x6c7967656e657261
v3 = 0x7465646279746573
...
v3 < return $ v3 `xor` k1;
v2 < return $ v2 `xor` k0;
v1 < return $ v1 `xor` k1;
v0 < return $ v0 `xor` k0;
...
 Initialize rest of SipState:
let mPart = 0
bytesRemaining = 8
inlen = 0
SipState{ .. } < return $ hash (SipState { .. }) a
let !b = inlen `unsafeShiftL` 56
v3 < return $ v3 `xor` b
 for( i=0; i
Congratulations, Don!For over two decades, the Academy’s Silver Medals have recognised exceptional personal contributions from early to midcareer engineers who have advanced the cause of engineering in the UK. Three of the UK’s most talented engineers are to receive the Royal Academy of Engineering’s coveted Silver Medal for remarkable technical achievements in their fields, coupled with commercial success.They are the inventor of 3D printed surgical instruments, an indoor locationtracking technology pioneer, and the creator of the F# computer programming language. Full RAE Announcement. Spotted by Kevin Hammond.
I presented this logic puzzle on Wednesday:
There are two boxes on a table, one red and one green. One contains a
treasure. The red box is labelled "exactly one of the labels is
true". The green box is labelled "the treasure is in this box."
Can you figure out which box contains the treasure?
It's not too late to try to solve this before reading on. If you
want, you can submit your answer here:
The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:
Results
There were 506 total
responses up to Fri Jul 3 11:09:52 2015 UTC; I kept only the first
response from each IP address, leaving 451. I read all the "something
else" submissions and where it seemed clear I recoded them as votes
for "red", for "not enough information", or as spam. (Several people
had the right answer but submitted "other" so they could explain
themselves.) There was also one post attempted to attack my
(nonexistent) SQL database. Sorry, Charlie; I'm not as stupid as I
look.
66.52% 300 red
25.72 116 notenoughinfo
3.55 16 green
2.00 9 other
1.55 7 spam
0.44 2 redwithqualification
0.22 1 attack
100.00 451 TOTAL
Onequarter of respondents got
the right answer, that there is not enough information
given to solve the problem, Twothirds of respondents said the
treasure was in the red box.
This is wrong. The treasure
is in the green box.
What?
Let me show you. I stated:
There are two boxes on a
table, one red and one green. One contains a treasure. The red box
is labelled "exactly one of the labels is true". The green box is
labelled "the treasure is in this box."
The labels are as I said. Everything I told you was literally true.
The treasure is definitely not in the red box.
No, it is actually in the green box.
(It's hard to see, but one of the items in the green box is the gold
and diamond ring made in Vienna by my greatgrandfather, which is
unquestionably a real treasure.)
So if you said the treasure must be in the red box, you were simply
mistaken. If you had a logical argument why the treasure had to be in
the red box, your argument was fallacious, and you should pause and try
to figure out what was wrong with it.
I will discuss it in detail below.
Solution
The treasure is undeniably in the green box. However, correct answer to the
puzzle is "no, you cannot figure out which box contains the
treasure". There is not enough information given. (Notice that the
question was not “Where is the treasure?” but “Can you figure out…?”)
(Fallacious) Argument A
Many people erroneously conclude that the treasure is in the red box,
using reasoning something like the following:
Suppose the red label is true. Then exactly one label is true,
and since the red label is true, the green label is false. Since it
says that the treasure is in the green box, the treasure must really
be in the red box.
Now suppose that the red label is false. Then the green label
must also be false. So again, the treasure is in the red box.
Since both cases lead to the conclusion that the treasure is in
the red box, that must be where it is.
What's wrong with argument A?
Here are some responses people commonly have when I tell them that
argument A is fallacious:
"If the treasure is in the green box, the red label is lying."
Not quite, but argument A explicitly considers the possibility
that the red label was false, so what's the problem?
"If the treasure is in the green box, the red label is
inconsistent."
It could be. Nothing in the puzzle statement ruled this out. But actually it's not inconsistent, it's just irrelevant.
"If the treasure is in the green box, the red label is
meaningless."
Nonsense. The meaning is plain: it says “exactly one of these labels is
true”, and the meaning is that exactly one of the labels is true.
Anyone presenting argument A must have understood the label to
mean that, and it is incoherent to understand it that way and then
to turn around and say that it is meaningless! (I discussed this point in more detail in 2007.)
"But the treasure could have been in the red box."
True! But it is not, as you can see in the pictures. The puzzle does
not give enough information to solve the problem. If you said that
there was not enough information, then congratulations, you have the
right answer. The answer produced by argument A is
incontestably wrong, since it asserts that the treasure is in the red
box, when it is not.
"The conditions supplied by the puzzle statement are inconsistent."
They certainly are not. Inconsistent systems do not have models, and
in particular cannot exist in the real world. The photographs above
demonstrate a realworld model that satisfies every condition posed
by the puzzle, and so proves that it is consistent.
"But that's not fair! You could have made up any random garbage at all, and then told me afterwards that you had been lying."
Had I done that, it would have been an unfair puzzle. For
example, suppose I opened the boxes at the end to reveal that there
was no treasure at all. That would have directly contradicted my
assertion that "One [box] contains a treasure". That would have been
cheating, and I would deserve a kick in the ass.
But I did not do that. As the photograph shows, the boxes,
their colors, their labels, and the disposition of the treasure are
all exactly as I said. I did not make up a lie to trick you; I described a real
situation, and asked whether people they could diagnose the location of
the treasure.
(Two respondents accused me of making up lies. One said:There is no
treasure. Both labels are lying. Look at those boxes. Do you really
think someone put a treasure in one of them just for this logic
puzzle? What can I say? I _did_ do this. Some of us just have higher
standards.)
"But what about the labels?"
Indeed! What about the labels?
The labels are worthless
The labels are red herrings; the provide no information. Consider the
following version of the puzzle:
There are two boxes on a table, one red and one green. One contains a
treasure.
Which box contains the treasure?
Obviously, the problem cannot be solved from the information given.
Now consider this version:
There are two boxes on
a table, one red and one green. One contains a treasure. The red box
is labelled "gcoadd atniy fnck z fbi c rirpx hrfyrom". The green box
is labelled "ofurb rz bzbsgtuuocxl ckddwdfiwzjwe ydtd."
Which box contains the treasure?
One is similarly at a loss here.
(By the way, people who said one label was meaningless: this is what a
meaningless label looks like.)
There are two boxes on a table, one red and one green. One contains a
treasure. The red box is labelled "exactly one of the labels is
true". The green box is labelled "the treasure is in this box."
But then the janitor happens by. "Don't be confused by those labels,"
he says. "They were stuck on there by the previous owner of the
boxes, who was an illiterate shoemaker who only spoke Serbian. I
think he cut them out of a magazine because he liked the frilly borders."
Which box contains the treasure?
The point being that in the absence of additional information, there
is no reason to believe that the labels give any information about the
contents of the boxes, or about labels, or about anything at all.
This should not come as a surprise to anyone. It is true not just in
annoying puzzles, but in the world in general. A box labeled “fresh figs” might contain fresh figs, or spoiled figs, or angry hornets, or nothing at all.
Order
What is the Name of this Book?
with kickback
no kickback
Why doesn't every logic puzzle fall afoul of this problem?
I said as part of the puzzle conditions that there was a treasure in
one box. For a fair puzzle, I am required to tell the truth about the
puzzle conditions. Otherwise I'm just being a jerk.
Typically the truth or falsity of the labels
is part of the puzzle conditions. Here's a typical example,
which I took from Raymond Smullyan's What is the name of this
book? (problem 67a):
… She had the following inscriptions put on the caskets:
GoldSilverLead
THE PORTRAIT IS IN THIS CASKET
THE PORTRAIT IS NOT IN THIS CASKET
THE PORTRAIT IS NOT IN THE GOLD CASKET
Portia explained to the suitor that of the three statements, at most one was true. Which casket should the suitor choose [to find the portrait]?
Notice that the problem condition gives the suitor a certification
about the truth of the labels, on which he may rely. In the quotation
above, the certification is in boldface.
A wellconstructed puzzle will always contain such a certification,
something like “one label is true and one is false” or “on this
island, each person always lies, or always tells the truth”. I went to
_What is the Name of this Book?_ to get the example above, and found
more than I had bargained for: problem 70 is exactly the annoying boxes problem!
Smullyan says:
Good heavens, I can take any number of caskets that I please and put
an object in one of them and then write any inscriptions at all on the
lids; these sentences won't convey any information whatsoever.
(Page 65)
Had I known that ahead of time, I doubt I would have written this post at all.
But why is this so surprising?
I don't know.
Final notes
16 people correctly said that the treasure was in the green box. This
has to be counted as a lucky guess, unacceptable as a solution to a
logic puzzle.
One respondent referred me to a similar
post on lesswrong.
I did warn you all that the puzzle was annoying.
I started writing this post in October 2007, and then it sat on the
shelf until I got around to finding and photographing the boxes. A
triumph of procrastination!
Here is a logic puzzle. I will present the solution on Friday.
There are two boxes on a table, one red and one green. One contains a
treasure. The red box is labelled "exactly one of the labels is
true". The green box is labelled "the treasure is in this box."
Can you figure out which box contains the treasure?
The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:
Starting on 20150703, the solution
will be here.
June 2015June 30th, 2015: Count Dracula has just enough time for a quickie, and today's #haskell problem http://lpaste.net/8137099602819022848 Count Dracula: "Vithd you, never a quickie ... alwayz a longie! Blablahblaaaah!" ... and the solution http://lpaste.net/7601734639496986624June 29th, 2015: Toodlepip! Wordfrequency of a novel purportedly written in 'Hinglish, don't you know!' http://lpaste.net/7805322136641339392 Today's #haskell problem That solution is SO my bag!http://lpaste.net/7435942974816518144June 26th, 2015: THUGs hate code duplication. I bet you didn't know that about THUGs. #thuglife With today's #haskell problem, you do. http://lpaste.net/87111690633609216 The solution is awesome, because reasons. http://lpaste.net/3951774515419152384June 25th, 2015: We solve today's #haskell problem like a Thug. A CANADIAN Thug http://lpaste.net/183406472317632512 … #ThugLife When a THUG wants a cupojoe, it just makes sense to give'm dat cupojoe when he throws down dat Hamilton http://lpaste.net/8960298568350957568 #thuglifeJune 24th, 2015: Today's #haskell problem shows us Mad Dad is Sad ... http://lpaste.net/1360790418425380864 … ... AND CANADIAN! AND SO ARE YOU! #whendidthathappenJune 23rd, 2015: Banana Fish! I don't know what that means, but: http://lpaste.net/4698665561507233792 (I also don't know what map 'a'"apple" 'b'"banana" means, either). Dad even got the banana WITH TAXES! http://lpaste.net/51803352903712768 But is Dad happy? Oh, no! See today's problem (forthcoming)June 22nd, 2015: A couple of rangelike thingies for today's #haskell problem http://lpaste.net/9214672078085554176 'Thingies' is a technical term. Arrows for ranges? http://lpaste.net/3818460590272151552 Who knew that could be a 'thing'? (Again, technical term. It means: 'thing.')June 19th, 2015: ♫ Grease is the word,is the word,is the word,that you heard,..http://lpaste.net/5444203916235374592... and is today's #haskell problem. #graph O! What a tangled web we weave! http://lpaste.net/1406493831142047744 Contracts between corporations #graph Using #neo4j to show complex interrelationships between corporations #haskellJune 18th, 2015: Graph owners of companies ... LIKE A BOSS for today's #haskell problem http://lpaste.net/8745167156892663808 def #NSFWyoutubelink: Take this #graph and shove it; I don' work here anymore! A solution http://lpaste.net/497988783522709504June 17th, 2015: What does Hannibal Lecter have to do with today's #Haskell problem? http://lpaste.net/3911201767555072000 Well, actually nothing. Good for namedropping ;)Ooh! pritti colours! Lines and circles! ME. LIKEY! http://lpaste.net/1108939510487449600 Visualizing relations between companies and their employees in #neo4j #graph database #bigdataJune 16th 2015: Business. Commerce. Relationships. And the plot thickens for today's #haskell problem http://lpaste.net/2159896812155043840 You scratched my back, so the solution will scratch yours: http://lpaste.net/6209720607693602816June 15th, 2015: We're told to 'mind our own business.' For today's #haskell problem, however, we don't. http://lpaste.net/409939376974331904 If all the world were 450 businesses ...huh, don't know how to end that couplet, so I'll just share the solution: http://lpaste.net/4134898821270339584June 12th, 2015: Today's Haskell problem is really simple: http://lpaste.net/176873973089304576 Write a Haskell Database. ;)June 11th, 2015: A mapping of a map of categories to various sets of symbols. Not at all a Graph. Nope. Not at all. http://lpaste.net/106990139309293568 So, forewarning: there is wootage to be found in the solution http://lpaste.net/1443717939034324992 June 10th, 2015: FREE LATIN LESSONS with today's #haskell problem! AND curl, but as long as you don't sudo bash you should be okay ... http://lpaste.net/8023684639111512064June 9th, 2015: LET'S PRETEND! that today is yesterday, huh? So 'today's #haskell problem is about Options Tradinghttp://lpaste.net/3308567286981328896 ... not really.June 8th, 2015: Improving the accuracy of the stddev modifier is the topic for today's #haskell problem http://lpaste.net/2181777565994188800June 5th, 2015: Today's #haskell problem is kinda from Haskell by Example http://lpaste.net/1846897956607754240 Maps don't love you like I love you Hey, did you just make a map from a map and a multimap? http://lpaste.net/1944556995998646272 Is that even allowed? Yes, ... yes, it is.June 4th, 2015: Peano's big TOE has a #haskell problem for you today, rollin' on the river http://lpaste.net/8694895204643110912 Types can be ... helpful in modeling solutions. Yeah. http://lpaste.net/6112991888283795456June 3rd, 2015: As we're not going to do switch for today's #haskell problem (Why? BECAUSE I SAID SO), let's deredundancify an array. http://lpaste.net/2725173830396936192 An array by any other name is just a graph http://lpaste.net/6699309431617748992 ... hey, it's possible!June 2nd, 2015: Today's #haskell problem is called 'twixt' and is inspired from a tweet by @jamestanton http://lpaste.net/4168110918607044608 Betwixt a rock and a prime place lies the solution http://lpaste.net/5331587919524134912June 1st, 2015: These factorials are prime for ... primes. Erhm, yeah. http://lpaste.net/6303441488491577344 Today's #haskell problem from @jamestanton
Start with Java, then:Forbid using null;Use only immutable objects, add "final" modifier to everything;Swap methods by static functions with the the original "this" as the first argument, e.g. "foo.bar()" turns into "bar(foo)";Add a lot of features to the type system; Remove type annotations, i.e. "Foo bar(Foo self)" turns into "bar(self)"; Remove useless parens, i.e. "bar(foo)" turns into "bar foo";Add callbyneed evaluation; Done, you have Haskell.It's not that hard, is it?One, using null references is a recognized bad practice, see "Null References: The Billion Dollar Mistake." Java 8 already provides the Optional type to stop using nulls.Two, immutable objects are a win strategy, see posts by Hirondelle Systems, IBM, Yegor, and others.Three, as you only have immutable objects, there is no reason to use methods instead of static functions, considering you maintain polymorphism (not quite the case for Java, but for the sake of this rant, consider as if it has this feature).Four, improve the type system. The type system used by Java language misses a lot of features. If you don't feel it, just consider this as an added bonus. When you start using the type system features in your favor, you end up with much better code. Five, imagine the Java compiler could infer the type of the arguments, so you don't need to type them everywhere. You still have the same static typing language, you just don't need to write the types. Shorter code means less liability to haunt you.Six, why all those parens? Just drop them. Less code to write, hurray!Seven, callbyneed just makes a lot of things easier (also makes a lot of things harder), but I really think it is a winner when you talk about productivity. When coding, I feel it a lot easier to express things in terms of values instead of steps (mathematicians have been doing this since long before computers). Expressing things in terms of values in a universe without callbyneed will result in a lot of useless computations, so callbyneed is a must.Eight, done! This is Haskell. No functors, monads, arrows, categories or lists needed.Why this post? Well, I don't know. It just occurred to me that if you really go into following good coding practices in Java (e.g. avoid null, use immutable objects), you will eventually feel familiar with functional code. Add some more things to the mix, and you end up with Haskell. I think people feel a bit scared at first contact with Haskell (and family) because of the academic and mathematical atmosphere it has, but in the end it is just a lot of good practices that you are kind of required to comply with.
Elsen is building the next generation of market simulation software at the intersection of high performance computing, machine learning, and quantitative finance. We're a small, tightknit team located in the financial district of downtown Boston.
We are looking for a senior software developer to help extend our infrastructure which is written in Haskell, C, and Python. Although substantial knowledge of Haskell is desired, we are primarily looking for individuals with demonstrated experience in financial modeling and the ability to implement ideas quickly and accurately.
Some things we look for in an candidate:
Open source involvement
Deep understanding of quantitative modeling
PostgreSQL or similar database familiarity
Understanding of various parallelism techniques (threads, software transactional memory, GPUs, distributed computing)
Technical analysis with talib
Use of iteratee Haskell libraries (conduit/pipes)
Experience with modern C development
NumPy/SciPy/Pandas experience
Open to playing complex board games from time to time
Overall funloving personality and good sense of humor
Get information on how to apply for this position.
20150630T20:36:06Z
Bezier curvesIt’s been a while I’ve been wanting to do that. Now it’s done! smoothie, a Haskell package for dealing with curves and splines, updated to version 0.3.That version introduces several changes. If you’re a good programmer, you might already have noticed that the major version got incremented. That means there’re compatibility breaking changes. If you don’t know what I’m talking about, you should definitely read this.The first – nonbreaking – change is that the package now supports Bézier interpolation! I’ve been reading about Bézier curves for a while because there’re very present and important for animation purposes – think of Blender. Feel free to dig in the documentation on hackage for further details.The second – breaking – change is that the interface has changed, especially the implementation of splines. However, the interface is now simpler and doesn’t require a lot of change in your code if you’ve been using older versions.Feel free to read the CHANGELOG for technical hints.As always, tell me what you think of the library, and keep the vibe!
Support for Mac users!This will be a short announcement about al, a Haskell wrapper to the OpenAL C library.Currently, the wrapper has been successfully tested on Linux – at least it works well on my Archlinux distro. I made a little program that reads from an .ogg file and streams the PCM signal to the wrapper – see libvorbis for further details. I’ll release the program later on if I find the spare time.The wrapper might also work on Windows as long as you have pkgconfig installed. I’d be very happy with feedback from people working on Windows. I don’t want anyone be put apart with my packages.However, I’ve never tested the wrapper on Mac OS X. I guessed it wouldn’t work out of the box because Mac OS X doesn’t use regular libraries to compile and link – that would have been too easy otherwise, and hell, think different right? They use something called a framework. It’s possible to include a framework in a Haskell project by fulfilling the frameworks field in the .cabal file. I received a simple patch to do that – here, and I merged it upstream.Then, Mac OS X is now officially supported. The release version is the 0.1.4.About stackageThere’s something else I’d like to discuss. Quickly after the first release of al, I decided to push it onto stackage. Unfortunately, there’s a problem with the package and Ubuntu. For a very dark reason, Ubuntu doesn’t expose anything when invoking pkgconfg cflags, even if the files are there – on Ubuntu they can be found in /usr/include/AL.That’s very silly because I don’t want to hardcode the location – it might be something else on other Linux distro. The problem might be related to the OpenAL support in Ubuntu – the .pc file used by pkgconfig might be incomplete. So if you experience that kind of issue, you can fix it by passing the path to your OpenAL headers:cabal install al extraincludedirs=/usr/include/ALIf OpenAL is installed somewhere else, consider using:find / name al.hI’ll do my best to quickly fix that issue.
Corporate and Employee RelationshipsBoth Graphical and Tabular ResultsSo, there are many ways to view data, and people may have different needs for representing that data, either for visualization (in a graph:nodeedgesview) or for tabulation/sorting (in your standard spreadsheet view).So, can Neo4J cater to both these needs?Yes, it can.Scenario 1: Relationships of owners of multiple companiesLet's say I'm doing some data exploration, and I wish to know who has interest/ownership in multiple companies? Why? Well, let's say I'm interested in the PeterPaul problem: I want to know if Joe, who owns company X is paying company Y for whatever artificial scheme to inflate or to deflate the numbers of either business and therefore profit illegally thereby.Piece of cake. Neo4J, please show me the owners, sorted by the number of companies owned:MATCH (o:OWNER)(p:PERSON)[r:OWNS]>(c:CORP)RETURN p.ssn AS Owner, collect(c.name) as Companies, count(r) as Count ORDER BY Count DESCDiagram 1: Owners by Company OwnershipBoom! There you go. Granted, this isn't a very exciting data set, as I did not have many owners owning multiple companies, but there you go.What does it look like as a graph, however?MATCH (o:OWNER)(p:PERSON)[r:OWNS]>(c:CORP)[:EMPLOYS]>(p1) WHERE p.ssn in [2879,815,239,5879] RETURN o,p,c,p1Diagram 2: Some companies with multiple ownersTo me, this is a richer result, because it now shows that owners of more than one company sometimes own shares in companies that have multiple owners. This may yield interesting results when investigating associates who own companies related to you. This was something I didn't see in the tabular result.Not a weakness of Neo4J: it was a weakness on my part doing the tabular query. I wasn't looking for this result in my query, so the table doesn't show it.Tellingly, the graph does.Scenario 2: Contractrelationships of companies Let's explore a different path. I wish to know, by company, the contractualrelationships between companies, sorted by companies with the most contractualrelationships on down. How do I do that in Neo4J?MATCH (c:CORP)[cc:CONTRACTS]>(c1:CORP) RETURN c.name as Contractor, collect(c1.name) as Contractees, count(cc) as Count ORDER BY Count DESCDiagram 3: ContractualRelationships between companiesThis is somewhat more fruitful, it seems. Let's, then, put this up into the graphview, looking at the top contractor:MATCH (p:PERSON)(c:CORP)[:CONTRACTS*1..2]>(c1:CORP)(p1:PERSON) WHERE c.name in ['YFB'] RETURN p,c,c1,p1Diagram 4: ContractualRelationships of YFBLooking at YFB, we can see contractualrelationships 'blossomout' from it, as it were, and this is just immediate, then distance 1 from that out! If we go out even just distance 1 more in the contracts, the screen fills with employees, so then, again, you have the foresttrees problem where too much data is hiding useful results with data.Let's prune these trees, then. Do circular relations appear?MATCH (c:CORP)[:CONTRACTS*1..5]>(c1:CORP) WHERE c.name in ['YFB'] RETURN c,c1Diagram 5: Circular Relationship found, but not in YFB! Huh!Well, would you look at that. This shows the power of the visualization aspect of graph databases. I was examining a hotspot in corporate trades, YFB, looking for irregularities there. I didn't find any, but as I probed there, a circularity did surface in downstream, unrelated companies: the obvious one being between AZB and MZB, but there's also a circularrelationship that becomes apparent starting with 4ZB, as well. Yes, this particular graph is noisy, but it did materialize an interesting area to explore that may very well have been overlooked with legacy methods of investigation.Graph Databases.BAM.
Sydney Padua explores an alternate universe wherein Ada Lovelace and Charles Babbage complete the Analytical Engine and use it to (at the order of Queen Victoria) fight crime. I've blogged before about the web comic, but the book is even better.Padua's tome reconciles hilarity with accuracy. I am not normally a fan of footnotes: if it is worth saying, say it inline; don't force your poor reader to break the flow of thought and eye, and leap to the bottom of the page. But here is the glorious exception, where the footnotes supplement, argue with, and occasionally threaten to overflow the comic. Even the footnotes have footnotes: endnotes cite sources for the dialogue, present pocket biographies of Ada and Charles' contemporaries Isambard Kingdom Brunel, Charles Dodgson, and George Boole, quote at length from original sources, and explain the workings of the Analytic Engine. In the midst of an illustrated fantasia riff on Alice in Wonderland, the footnotes pursue an academic war as to whether or not Babbage truly considered Lovelace to be the Empress of Number. Padua makes pursuit of Victorian arcana a thrilling adventure of its own. Highly recommended!
Since the release of the stack build
tool,
I think I've received four different requests and bug reports about stack
support in Yesod. The sticking point is that yesod devel has not until now
had support for using stack. The original plan was to wait for Njagi Mwaniki's
Google Summer of Code project to finish the new idebackend based yesod devel.
However, demand for this feature was too high, so I'm happy to announce
official stack support in yesodbin1.4.11.This blog post should be consider a beta announcement for using Yesod with
stack. Please test and report issues. Also, the workflow is not yet perfected.
Once we get stack new
written and add idebackend
support, things will be
much smoother. For now, here's the workflow:# Install both yesodbin and cabalinstall. Both are still necessary
$ stack install yesodbin1.4.11 cabalinstall
# Initialize your project
$ stack exec yesod init
$ cd newdirectory
# Create stack.yaml
$ stack init
# Build your project to get al dependencies
# Also rebuild yesodbin with the current GHC, just to be safe
$ stack build yesodbin1.4.11 .
# Now run yesod devel
$ stack exec yesod develLike I said, this is a little kludgy right now, but will smooth out over time.Technical detailsIf you're curious in how I added this support, the commit is really
short.
And there's not actually anything stackspecific in here, it's just working
around a well known limitation in cabal which makes it incompatible with the
GHC_PACKAGE_PATH environment variable. All we do in yesod devel is:Detect the GHC_PACKAGE_PATH variableTurn it into packagedb arugments to cabal configureRemove GHC_PACKAGE_PATH from the environment of the cabal processIt would be nice if cabal got this functionality itself in the future, but I
believe the current implementation was a design goal of the cabal team.