Thursday, March 9, 2017

Writer comonad in Coq

In the last post, we reviewed Writer comonad in Haskell. In this post we will implement it in Coq. Since monads are not the part of standard Coq library, and we will use ExtLib which provide basic monad definitions.

First, we need to define Writer monad. ExtLib only provides WriterT monad transformer, from which we can trivially create a Writer monad:

Variable s t : Type.
Variable Monoid_s : Monoid s.

Definition writer := writerT Monoid_s ident.
Definition runWriter x := 
   unIdent (@runWriterT s Monoid_s ident t x).
Definition execWriter x:= psnd (runWriter x).
Definition evalWriter x:= pfst (runWriter x).

Here, we define `writer` type constructor and `runWriter` method.  Additionally, we define a couple of convenience methods on top of `runWriter` to extract state and the value from the results of unwrapping the monad.

ExtLib has CoMonad class defined as:

Class CoMonad (m : Type -> Type) : Type :=
{ coret : forall {A}, m A -> A
; cobind : forall {A B}, m A -> (m A -> B) -> m B

The first thing you notice is that the names are different from the ones we've seen in Haskell. They reflect category theory duality between monads and comonads. Essentially 'coret' is 'extract,' and 'cobind' is 'extend' with slightly different argument order. For now, let us stick to these definitions. We define a Writer comonad as:

Variable w: Type.
Variable m: Monoid w.

Global Instance WriterCoMonad:  CoMonad (@writer w m) := {
  coret A x := evalWriter x ;
  cobind A B wa f := tell (execWriter wa) ;; ret (f wa)

The definition is pretty much the same as we wrote in Haskell except for the adjustments for Coq/ExtLib monad syntax.

Since we are in Coq, in addition to defining the comonad we can formalize comonad laws and prove that our implementation complies with them. Unfortunately, `cobind` argument's order make the formulation of comonad rules little clumsy, so we will first define wrappers reverting it to familiar Haskell's name and argument order:

Variable m : Type -> Type.
Variable C : CoMonad m.

Definition extract {A:Type}: (m A) -> A := @coret m C A.
Definition extend {A B:Type} (f: m A -> B): m A -> m B  :=
    fun x => @cobind m C A B x f.

Now we can define CoMonadLaws class which specifies the rules:

Class CoMonadLaws : Type := {
  extend_extract: forall (A B:Type),   extend (B:=A) extract = id ;
  extract_extend: forall (A B:Type) {f},   extract  (@extend A B) f = f;
  extend_extend: forall (A B:Type) {f g}, (@extend B A) f  (@extend A B) g = extend (f  extend g)

Finally, we will prove that our WriterComonad satisfies these rules by instantiating this class and proving the rules. To do this, we need to assume that the proof is provided that underlying monid instance used in our Writer complies to MonoidLaws.

Variable ml: MonoidLaws m.

Global Instance WriterCoMonadLaws:
    CoMonadLaws (@WriterCoMonad).
      intros A B.
      unfold extract, extend.
      extensionality x.
      unfold coret, cobind, WriterCoMonad, id.
      unfold evalWriter, execWriter, runWriter.
      destruct x, runWriterT, unIdent.
      repeat f_equal.
      apply ml.
      intros A B f g.
      unfold extract, extend, compose.
      unfold coret, cobind, WriterCoMonad.
      extensionality x.
      repeat f_equal.
      apply ml.

For clarity in the code snippets above, I have omitted some auxiliary code. You can look at the full example at WriterComonad.v.

Wednesday, March 8, 2017

Writer comonad in Haskell

Writer monad is readily available in Haskell. But what about Writer comonad? Let us start with the basics. Comonad class is defined as:

Comonad w where
    extract :: w a -> a
    duplicate :: w a -> w (w a)
    extend :: (w a -> b) -> w a -> w b

The minimal implementation requires you to implement 'extract' and 'extend.'  Additionally, it must satisfy the following comonad laws:

extend extract      = id
extract . extend f  = f
extend f . extend g = extend (f . extend g)

The 'extract' is pretty straightforward -- it allows safely extract value from the monad:

extract x = fst $ runWriter x

Our first intuition for 'extend' would be something like this:

extend f wa = return (f wa)

Which is incorrect, as it losses the state accumulated so far and replaces it with 'mempty' and thus do not satisfy the 1st law above (extend extract = id).

Without further ado, the writer comonad definition below correctly preserves the state and meets all three laws:

instance (Monoid w) => Comonad (Writer w) where
    extract x = fst $ runWriter x
    extend f wa = (tell $ execWriter wa) >> return (f wa)


  1. Haskell comonad library
  2. Category Theoretical view of comonads
  3. Another implementation of Writer and Reader comonads in Haskell

Friday, January 13, 2017

Switching between 3 languages in Ubuntu

I use three languages: English, Russian, and Ukrainian.

Switching between them is a bit tricky. Usually, you type in one of them, occasionally switching to a second one. It is almost never you need to randomly switch between all 3. MacOS keyboard switching mechanism reflects that, with default keyboard language switch shortcut toggling between the two most recently used languages. If you want to switch to the 3rd one, you can use toolbar menu or a separate keyboard shortcut:

When I switched to Ubuntu, the first thing I've noticed is that input switch shortcut cycles through all 3 languages. This is very inconvenient. Of course, I wanted to replicate MacOS behavior. With a little help from Stack Exchange, I was able to do so. Save this script as `` somewhere and make sure it executable:

Then, go to "System Settings" > "Keyboard" > "Shortcuts" > "Custom Shortcuts". Click the "+" and add a custom shortcut to it. I use Alt-SPACE. It will cycle between last 2 languages.

P.S. Perhaps I should try to supply a patch or at least open a Gnome bug for this behavior. If anybody familiar with Gnome infrastructure could point me in a right direction I can work on this.

Wednesday, November 2, 2016

BitBucket Git checkout over SSH with multiple accounts

If you have multiple user accounts at BitBucket (e.g. personal and work), you may run into a problem. The first think you will notice that you could not use the same ssh key. Adding it to the second account will give you "the key is already used by someone else" error message. Now if you generate a new key and add it to your ssh-agent (via ssh-add), you will not be able to check out from one of your accounts.

The problem is caused by ButBucket identifying a user by first SSH key he or she supplies. There are several workarounds for this problem, but the one I prefer is to use ssh Host alias. In your ~/.ssh/config file add section like this:
Host bitbucket-cm
    User git
    IdentityFile ~/.ssh/id_rsa.1
    IdentitiesOnly yes
This would basically create a SSH host alias bitbucket-cm for associated with id_rsa.1 key. Now, instead of usual checkout URL, say, 
git clone 
git clone git@bitbucket-cm:org/repo.git

Wednesday, July 13, 2016

Pokemon Go circa 2012

Looking at current Pokemon Go success (It added whopping $9B to company's capitalization) I could not help help looking back at another project we did few years ago.

Back in 2012 we, at Codeminders, were working on Computer Vision algorithms for mobile phones. At some point we realized that there is a potential for a business there and developed a demo and even pitched to some angel investors. The investors told us that the gaming aspect is not interesting, and we should focus on some real-life problems like real estate, etc. Eventually we just published a technology demo in app store and let it go.

To demonstrate location-based augmented reality gaming we have chosen Pikachu avatar which you can place at random locations, where your friends can find it. The unique part was that it worked indoors, not relying on GPS alone.

Here is an image from our investor's pitch:

You can see our presentation here (I've removed some boring slides related to financials and planning). Also you can try yourself our demo (Android version, iOS version). In the demo we replaced Pikachu with Squirrel to avoid infringing on Nintendo's trademarks.

Saturday, February 6, 2016

State Monad in Coq Tutorial

In this post we will review usage of StateMonad in Coq using ExtLib on an adapted example from  a Haskell State Monad tutorial.

We will implement a simple game function which takes a string from dictionary {a,b,c} and produces a score number. The game could have two modes: on and off. It consumes an input string character by character and updates the mode and the score at each step. Initially the mode is off. The character 'c' toggles the on/off mode flag. In off mode, consuming characters does not affect the score. In on mode, each occurrence of the character 'a' increases the score by 1, and each occurrence of the character 'b' decreases it by 1. So for example, the input sequence "ab" will result in a score of 0, "ca" a score of 1, "cabca" also a 0, and "abcaaacbbcabbab" will result in a score of 2.

Let us look the implementation of this game in Coq using State Monad:

1 Require Import Coq.ZArith.ZArith_base Coq.Strings.String.
2 Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
4 Section StateGame.
5   Import MonadNotation.
6   Local Open Scope Z_scope.
7   Local Open Scope char_scope.
8   Local Open Scope monad_scope.
10   Definition GameValue : Type := Z.
11   Definition GameState : Type := (prod bool Z).
13   Variable m : Type → Type.
14   Context {Monad_m: Monad m}.
15   Context {State_m: MonadState GameState m}.
17   Fixpoint playGame (s: string): m GameValue :=
18     match s with
19     |  EmptyString =>
20        v <- get ;;
21          let '(on, score) := v in ret score
22     |  String x xs =>
23        v <- get ;;
24          let '(on, score) := v in
25          match x, on with
26          | "a", true =>  put (on, score + 1)
27          | "b", true => put (on, score - 1)
28          | "c", _ =>   put (negb on, score)
29          |  _, _  =>    put (on, score)
30          end ;; playGame xs
31     end.
33   Definition startState: GameState := (false, 0).
34 End StateGame.
36 Definition main : GameValue :=
37   (evalState  
38            (playGame (state GameState) "abcaaacbbcabbab") startState).

I will omit description of the Coq nuts and bolts of Require, Import, and Open Scope instructions in lines 1-8.

In lines 10 and 11, we declare type aliases for our game score value as a signed integer (Z), and game state as a product of the boolean game mode and and an integer game score.

Variable 'm' in line 13 identifies our Monad by it's type constructor. Line 14 states that 'm' must be an instance of type class Monad. If we look at ExtLib's definition of this type class we will see that it just postulates the presence of the standard Monad bind and return (called ret here) functions:

Class Monad (m : Type → Type) : Type := { 
    ret : ∀ {t}, t → m t ;
    bind : ∀ {t u}, m t → (t → m u) → m u

The next class, mentioned in line 15 brings additional get and put definitions, specific for State Monad:

Class MonadState (T : Type) (m : Type → Type) : Type := {
    get : m T ;
    put : T → m unit

The actual game function definition begins on line 17. It is a recursive function consuming an input string and returning a monadic value as a result. The string is an inductive type and we match its two constructors on lines 19 and 22, respectively. If the string is empty, we use syntax x <- c1 ;; c2 which is a Coq's rendering of well a known do-notation. Informally: we extract a score element from the current state tuple and return it as a monadic value using ret. While in Haskell, we can write a much terser expression (_, score) <- get, in Coq we have to use an intermediate value 'v' followed by destructive let, which unfortunately does not allow us to use a wildcard for the first element (mode), which we do not need anyway.

In the case of the second constructor on line 22 we again use do-notation and destructing let to break down the current state into on and score components and then analyze their combinations via match. Again, we use slightly different syntax from Haskell's version and, instead of matching on x with guards, we match on both x and on. Depending on their combination, we update the score and on/off flag according to our game rules using the state monad's put function. Then, we proceed with the next recursive iteration chained by c1 ;; c2 notation which is sometimes called then operator (>>) in Haskell, and used to to chain monadic computations where c2 does not depend on the outcome of c1. This could be expanded into our familiar do-notation of:  _ <- c1 ;; c2.

On line 33, we define our initial game state (game off, score=0) as startState.

On line 36, we define our 'main' function, which runs a game for a specific string and returns an integer score. It is a bit difficult to parse, so for clarity let us split it into several definitions, specifying return types and making all arguments explicit via '@':

Definition m : Type → Type := state GameState.
Definition pg :  state GameState GameValue := @playGame m _  _ "abcaaacbbcabbab".
Definition main : GameValue := @evalState GameState GameValue pg startState.

The first definition 'm' uses the state record type to create our State Monad's constructor. It is defined as:

state: Type → Type → Type
Record state (S t : Type) : Type := mkState { runState : S → t * S }

We partially specialize state with GameState, which gives us a new type constructor (Type → Type), which instantiates a type which holds a function with a type GameState -> t * GameState.

Th next definition 'pg' holds a monadic value returned as a result of running our game. You may notice that its type is state GameState GameValue which is the same as m GameValue, the type of  playGame. Please note that playGame was defined inside a section. Consequently, when seen outside one, it is additionally universally quantified with all section variables. In our case playGame now takes 4 arguments. The first is a type constructor for the monad, the second is the type class instance Monad m that carries the monad functions, the third is the type class instance MonadState GameState m that carries the monad state functions, and the fourth is the string input to the function. We explicitly provide 'm' but use wildcards for type class parameters, letting the type class resolution mechanism find instances for parameters marked as _ . Coq will look for a type class instance of Monad (state GameState) and MonadState (state GameState). Both of these are defined as Global Instances in the ExtLib.Data.Monads.StateMonad library so type class resolution finds the definitions. Thus, after class resolution, the 'pg' definition will expand to:

(@playGame (state GameState) (Monad_state GameState)
     (MonadState_state GameState) "abcaaacbbcabbab"

Finally in the 'main' definition, we use the evalState function to get our result. It is defined as:

Definition evalState {t} (c : state t) (s : S) : t :=
    fst (runState c s).

The semantics are pretty straightforward; we apply State Monad to the initial state (run state transition function), and project out the first element of the returned tuple (the score).

To test our implementation we can use Compute main instruction to get the expected result (2).

P.S. I would like to thank Gregory Malecha for the explanations, comments, and suggestions he provided.

Thursday, February 4, 2016

Auqamacs, Proof General and company-coq

If you are using Coq under Emacs, you are most likely using Proof General (note the new link, they moved to github recently). If you are not using excellent CompanyCoq extension to PG by Clément Pit--Claudel, you certainly should! (I was wondering for a while why it is named "company". The answer is that it is based on eponymous text completion framework for Emacs. The name stands for "complete anything".)

Aquamacs is a version of Emacs popular among MacOS X users. Unfortunately some key binding from company-coq do not work under it. Specifically control-mouse-1 which should show an overlay popup with information about a clicked symbol. There is a ticket open and there is a helpful discussion with developers but it looks like we could not make it work as on other platforms. There is a workaround described below, but I am not sure if it is going to make it to official release. If it does not or until it does here is what you can do. Add the following to your .emacs:

(add-hook 'coq-mode-hook
          (lambda ()
            (company-coq-initialize) ;; Load company-coq when opening Coq files
            (if (boundp 'aquamacs-version)
                  (define-key company-coq-map (kbd "<c-down-mouse-3>") #'company-coq-show-definition-overlay-under-pointer)
                  (define-key company-coq-map (kbd "<c-mouse-3>") #'company-coq-clear-definition-overlay)))))

The difference from other emacsen is that you need to use control-right-mouse-click. On MacBook's touchpad it means holding Control button while clicking on touchpad with two fingers. If you are using Apple Magic Mouse, click with one finger, but on the right side of the mouse. Finally if you are using 3-button USB mouse, you should click on right button, although I have not tested this.