Basics for a modular arithmetic type in Agda

In my prevous post, I described a zipper-like representation for modular counters. That representation was well-suited for when your only operations are incrementing and decrementing. However, it'd be really cumbersome to do more complex arithmetics with it.

Then the next week, Peter Diviánszky told me about all the cool stuff that was presented at the latest Agda Implementors' Meeting, among them, the Quotient library. I still remember the time when, as a practice, I tried to implement integers in Agda without looking at the standard library. I came up with something much like the library representation, except mine had a separate constructor for zero (so I had +1+ n and -1- n). I really hated how I had to shift by one at least one of the cases to avoid ending up with two representations of zero. If only there was a way to tell Agda that those two representations actually mean the same thing...

Quotient types promise to do just that: you define a type where the constructors may be redundant so that there may be several values that should have the same semantics, and then you divide it with an equivalence relation so that the new type's values are the equivalence classes. See this example defining integers as pairs of natural numbers such that the pair (x, y) represents x-y.

I wanted to try doing the same for a proper modular integer type, by factoring integers with the equivalence relation x ∼ y ⇔ n ∣ ∣x-y∣. The point is, you take the integers, define this relation, then prove that it is indeed an equivalence (i.e. it is reflexive, symmetric and transitive), in other words, you create a setoid; then you use the Quotient type constructor to create your set-of-equivalence-classes type. After that's done, you can define functions over this quotient type by defining them over representations, and proving well-definedness, i.e. that the function maps equivalent representations to the same result.

This last step can be needlessly cumbersome when defining either non-unary functions or endomorphisms, so first of all I created a small library that makes it easier to define unary and binary operators over a quotient type. For example, to define a binary operator, all you need is a binary operator on the representation set, and a proof that the operator preserves the equivalence, thereby being agnostic to the choice of representant on both arguments:

    lift₂ : (f : Op₂ A₀) → f Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ → Op₂ (Quotient A)

So after writing loads and loads and loads of arithmetic proofs on divisibility of absolute values, like n ∣ ∣x∣ ∧ n ∣ ∣y∣ ⇒ n ∣ ∣x + y∣, I was finally ready to define modular addition:

Mod₀ : ℕ → Setoid _ _
Mod₀ n = {!!}

Mod : ℕ → Set
Mod n = Quotient (Mod₀ n)

plus : ∀ {n} → Mod n → Mod n → Mod n
plus {n} = lift₂ _+_ proof
  where
  proof : ∀ {x y t u} → n ∣ ∣x - y∣ → n ∣ ∣t - u∣ → n ∣ ∣(x + t) - (y + u)∣
  proof = {!!}
      

Of course, the meat of the work was in actually defining Mod₀ and proof above. But after that, we can get back our old increment/decrement functions as very simple and straightforward definitions:

_+1 : ∀ {n} → Mod n → Mod n
_+1 = plus [ + 1 ]

_-1 : ∀ {n} → Mod n → Mod n
_-1 = plus [ - (+ 1) ]
      

And proving that _+1 and _-1 are inverses of each other comes down to the very simple arithmetic proof (on vanilla integers!) that

pred-suc : ∀ x → ℤpred (ℤsuc x) ≡ x
      

Of course, much more properties need to be proven. The end goal of this project should be to prove that Mod n is a commutative ring; a much more ambitious project would be proving that Mod p is a field if p is prime. Unfortunately, on my machine Agda takes more than two minutes just to display the goal and context in the following hole:

plus-comm : ∀ {n} → (x y : Mod n) → plus x y ≡ plus y x
plus-comm {n} x y = {!!}
      

so this is a problem I'll have to find a workaround for before going on. But at least I have my counters, so I can at least get back to my original goal and work on the register machine semantics. Expect the next post to be about that.

You can browse the full source code here, and track it on GitHub.

Mod-N counters in Agda

First of all, before I start on the actual blog post, let me put this in context. I rembember a couple of years ago when I developed an interest in functional programming languages, and Haskell in particular. There was a phase when I was able to use Haskell to solve problems in the small. I understood most of the basics of pure functional programming; then there were things I regarded as magic; and of course there was a lot of things I didn't even know that I didn't know about. But none of it did I grok.

I feel like I'm starting to get to the same level with Agda now. So this is going to be one of those "look at this cool thing I made" posts where the actual result is probably going to be trivial for actual experts of the field; but it's an important milestone for my own understanding of the subject.

I wanted to play around with simple but Turing-complete languages, and I started implementing an interpreter for a counter machine. More on that in a later post; this present post describes just the representation of register values. In the model that I implemented, values of registers are byte counters, meaning they have 256 different values, and two operations +1 and -1 that the inverses of each other. Incrementing/decrementing should roll over: 255 +1 = 0 and 0 -1 = 255.

How I learned about Java's lack of type erasure the hard way

This week, I started playing around with the Android platform. I've been eyeing Yeti, an ML dialect that compiles to JVM and features structural typing. Even though I only have very limited experience in ML (mostly just reading the snippets in the Okasaki, and having helped Maya once with some F# code), it has to be better than Java, right?

After getting the hang of Yeti (integrating it into Android's ant build system, writing Hello World, etc.) I wanted to write something more substantial to evaluate the language for serious use. However, yesterday evening I started getting weird errors as soon as I started creating non-trivial closures in member functions. This is the chronicle of how I tracked down the problem with just some rudimentary Java knowledge and lots of reverse engineering.

Developing iPhone applications in Haskell — a tutorial

I couldn't find a step-by-step tutorial explaining the process of developing iOS applications in Haskell, so after finally getting "Hello World" to run on an iPhone, I decided to write this tutorial. I should also credit Lőry, who did the iOS side of the work.

The basic overview of what we're going to do in this tutorial is the following:

• Write the backend of our application in Haskell
• Create FFI bindings for our backend
• Use Jhc to compile the Haskell code into vanilla C
• Write the front-end using the official iOS SDK, using Objective-C
• Create wrappers on the Objective-C side to make resource managment easier
• Compile and link it all using Objective-C and C compilers targeting the iOS devices

Writing the backend in Haskell

For this tutorial, we will simulate an intricate Haskell backend with the a simple function. For your real application, this is where you go all out with your Haskell-fu.

module Engine where
      
import Data.Char (ord)
      
engine :: String -> Either String [Int]
engine s | length s < 10 = Left "String not long enough"
         | otherwise = Right $ map ord s
      

FFI bindings

To interface our backend with the frontend developed in Objective-C (or C or C++ or...), we need to represent the input and output of our Haskell function in terms of simple C types. For the function engine, a straightforward API would be, in pseudo-C:

bool engine (in string s, out string error, out int[] result)
      

Of course, we have to use char *'s for strings, and pointers for out parameters and arrays, so our real API will be:

int engine (char* s, char* *error, int* *result, int *result_length)
      

with engine returning 0 on success (Right) and non-zero on failure (Left).

The Haskell FFI representation of this signature is:

foreign export ccall "engine"
  engineC :: CString -> Ptr CString -> Ptr (Ptr CInt) -> Ptr CInt -> IO CInt
    

The next step requires us to actually define engineC that does all the necessary marshalling. We simply evaluate engine and then set the appropriate out-parameters.

module Engine.FFI (engineC) where
    
import Foreign
import Foreign.C
import Control.Monad (zipWithM_)
    
foreign export ccall "engine"
  engineC :: CString -> Ptr CString -> Ptr (Ptr CInt) -> Ptr CInt -> IO CInt
engineC s ptrErr ptrptrResult ptrLen = 
  do
    s' <- peekCString s    
    case engine s' of
      Left err -> do
        cErr <- newCString err
        poke ptrErr cErr
        return 1
      Right result -> do
        pokeList ptrptrResult ptrLen $ map fromIntegral result
        return 0      
    
pokeList :: Storable a => Ptr (Ptr a) -> Ptr CInt -> [a] -> IO (Ptr a)
pokeList ptrptrList ptrLen xs = 
  do
    let len = length xs
    ptr <- mallocBytes $ len * elemSize          
    let ptrs = iterate (`plusPtr` elemSize) ptr
    zipWithM_ poke ptrs xs 
    poke ptrptrList ptr
    poke ptrLen $ fromIntegral len
    return ptr
  where 
    elemSize = sizeOf $ head xs
    

Compiling Haskell to C

The next step is compiling our Haskell project into C, so that we can use Apple's SDK to compile that for the iPhone, and also call engine from other code, like the Objective-C parts that make up the frontend.

Unlike GHC, Jhc doesn't compile individual modules. Instead, it compiles every used definition (but only those) and the runtime into a single C source file. Although we are not going to run our Haskell program directly, and instead call to it from the frontend, Jhc still needs a main function in the source code. So let's create a Main module which we will compile with Jhc:

module Main where

import Engine.FFI

main :: IO ()
main = return ()    
    

We can compile this module into a C file containing the code for engineC and everything else it uses (including imported packages):

The -fffi flag turns on FFI support and makes Jhc generate the engine function from the foreign export declaration and the definition of engineC. Note that there is no name clash between engine the C function (defined as engineC in Haskell-land) and engine the Haskell definition. I think in this particular example it is cleaner to use the same name for both.

The -fjgc flag generates GC code. Note that we will also need to enable the GC code in the next step, when compiling the C sources.

The --cross -mle32 flags are important because they instruct Jhc to target little-endian, 32-bit CPUs which is what the ARM is.

Compiling the generated C source code

Everything up to this point can be done without Apple's SDK, and in fact you can run Jhc on any platform you wish. From here on, however, we will use the iOS SDK to compile to ARM.

To compile EngineMain.jhc.c, we first need to set some preprocessor macros:

• _GNU_SOURCE
• NDEBUG
• _JHC_GC=_JHC_GC_JGC (turns on the generated GC code)
• _JHC_STANDALONE=0 (this disables the main function defined in our module)

You also need some important C compiler flags (you can ignore the warning settings if you'd like):

-marm is very important because otherwise, GCC (or Clang) and Jhc step on each other's toes, leading to strange crashes seemingly out of nowhere.

Creating the frontend and accessing the backend

You can use the standard SDK to create the frontend; I will not cover that here in detail. You also need to create a header file containing the signature of our exported function. The code generated by Jhc also contains initialization and finalization routines that need to be called before and after calling any functions defined in Haskell:

extern void hs_init (int *argc, char **argv[]);
extern void hs_exit (void);

extern int engine (char* s, char* *msgError, int* *result, int *len);
      

You also need to manage the memory returned by the backend. The call to mallocBytes in the marshalling code is compiled into vanilla malloc, so you can simply call free after you're done with it.

To make initialization and memory management easier, Lőry has created a sample XCode project that wraps the C API to use Objective-C types. You can find the tarball here.

The case for compositional type checking

This is an based on a chapter of the M.Sc. thesis I am writing at ELTE, supervised by Péter Diviánszky.

For my M.Sc. thesis, I've been working on writing a compositional type checker for Haskell 98. The basic idea is to extend Olaf Chitil's compositional type system with ad-hoc polymorphism, Haskell 98's major extension to the Hindley-Milner type system. In this post, I'm showing the motivation behind wanting to go compositional.

A property shared by both commonly-used algorithms for doing Hindley-Milner type inference, W and M, is that both W and M infer the type of composite expressions by inferring one subexpression (in some sense, the “first” one) and using its results in inferring the type of the “next” one. They are linear in the sense that partial results are threaded throughout the type inference.

The effect of linearity on type inference is that certain sub-expressions (those that are processed earlier) can have greater influence on the typing of other subexpressions. This is bad because it imposes a hierarchy on the subexpressions that is determined solely by the actual type checking algorithm, not by the type system; thus, it can lead to misleading error messages for the programmer.

For example, let's take the following definition of a Haskell function:

There are two ways to typecheck this definition using W: either we first typecheck toUpper x, using the context {x :: α}, resulting in the type equation α ~ Char, then checking not x with {x :: Char}, or do it the other way around, by first looking at not x, then as a result recursing into toUpper x with the context {x :: Bool}.

GHC, it seems, does the former, resulting in the following error message:

Whereas Hugs 98 does the latter:

The problem is that they are both misleading, because there is nothing wrong with either not x or toUpper x by itself. The problem only comes from trying to unify their respective views on the type of x.

A compositional type checker, in contrast, descends into toUpper x and not x using the same context, {x :: α}. The first one results in the typing (which is defined to be not just the type of an expression, but also a mapping of monomorphic variables to their types) {x :: Char} ⊢ Char, and the second one in {x :: Bool} ⊢ Bool. Only afterwards are these two typings tried to be unified.

This is better because it becomes meaningful to talk about the typing of a subexpression. For the example above, my work-in-progress compositional type checker can report errors with an (IMO) much more helpful message:

Of course, the devil's in the details — but that's what my thesis will be about.