Resources on String Diagrams, and Adjunctions, and Kan Extensions

I’ve been trying to figure out Kan Extensions

Ralf Hinze on Kan Extensions

https://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

 

But while doing that I went down a rabbit hole on String Diagrams

This post is the first one on String Diagrams that made sense to me.

https://parametricity.com/posts/2015-07-18-braids.html

I had seen this stuff before, but I hadn’t appreciated it until I saw what Haskell expressions it showed equivalence between. They are not obvious equivalences

This seems like a very useful video on this topic.

https://skillsmatter.com/skillscasts/8807-categories-and-string-diagrams

In Summary, it is an excellent notation for talking about transformations of a long sequence of composed Functors  F G H … into some other long sequence of Functors. The conversion of functors runs from up to down. The composition of functors procedes left to right.  F eta is the fmap of eta, and eta F is eta with the forall’ed type unified to be of the form F a.

Adjunctions L -| R are asymmetric between cups and caps. L is on the left in cups and on the right in caps. That’s what makes squiggles pull straightable

I think I have an interesting idea for a linear algebra library based on this stuff

 

John Baez and Mike Stay’s Rosetta Stone (A touch stone I keep returning to)

math.ucr.edu/home/baez/rosetta.pdf

Dan Piponi gave a talk which is another touch stone of mine that I come back to again and again. There is a set of corresponding blog posts.

Other resources:

NCatLab article

https://ncatlab.org/nlab/show/string+diagram

John Baez hosted seminars

http://www.math.ucr.edu/home/baez/QG.html

Catsters

https://www.youtube.com/view_play_list?p=50ABC4792BD0A086

 

Dan Marsden’s Article

https://arxiv.org/abs/1401.7220

Marsden and Hinze have been collaborating

events.inf.ed.ac.uk/wf2016/slides/hinze.pdf

https://link.springer.com/chapter/10.1007/978-3-319-30936-1_8

Stephen Diehl on Adjunctions

http://www.stephendiehl.com/posts/adjunctions.html

 

A Section From an old Oregon Programming Language Summer School (a rich set of resources)

 

Marsden and Hinze have been collaborating

events.inf.ed.ac.uk/wf2016/slides/hinze.pdf

https://link.springer.com/chapter/10.1007/978-3-319-30936-1_8

 

Mike Stay doing a very interesting series of Category Theory in Javascript. He uses contracts in place of types. Defeats one of the big points of types (static analysis), but still pretty cool

 

 

I think that about covers everything I know about.

Oh yeah, there is the whole Coecke and Abramsky categorical quantum mechanics stuff too.

Using the Purescript Servant Bridge

Alright, here is some garbage code. Hope it helps you, sorry if it confuses you.

Checkout the Counter example

https://github.com/eskimor/servant-purescript/tree/master/examples/central-counter

that is where I pulled everything from. I ripped out just about everything fancy just so you and I can see the truly bare bones example.

It’s mostly boiler plate on the generator side.

He does a couple fancier things that you may want, like rearranging names and changing folders. Here is a more basic example

This goes in app/PSGenerator.ps if you’re using a stack template

{-# LANGUAGE AutoDeriveTypeable    #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}

module Main where

import           Control.Applicative
import           Control.Lens
import           Data.Aeson
import           Data.Monoid
import           Data.Proxy
import qualified Data.Set                           as Set
--import           Data.Text                          (Text)
import qualified Data.Text                          as T
import qualified Data.Text.Encoding                 as T
import qualified Data.Text.IO                       as T
import           Language.PureScript.Bridge
import           Language.PureScript.Bridge.PSTypes
import           Servant.API
import           Servant.PureScript
import           Servant.Subscriber.Subscribable

import qualified Lib


myBridge :: BridgePart
myBridge = defaultBridge

data MyBridge

myBridgeProxy :: Proxy MyBridge
myBridgeProxy = Proxy

instance HasBridge MyBridge where
  languageBridge _ = buildBridge myBridge

-- List all the types you want to end up in ServerTypes.purs Auto builds lenses too?
myTypes :: [SumType 'Haskell]
myTypes =  [
           mkSumType (Proxy :: Proxy Lib.User)
--          , mkSumType (Proxy :: Proxy Lib.Hello)
          ]

mySettings :: Settings
mySettings = defaultSettings

main :: IO ()
main = do
  let frontEndRoot = "frontend/src"
  writeAPIModuleWithSettings mySettings frontEndRoot myBridgeProxy Lib.userAPI'
  writePSTypes frontEndRoot (buildBridge myBridge) myTypes

Mostly things can just be the defaults. Look at the Counter Example for some more config stuff you can do.

You do need to separate out the user json api by itself. If you hand writeAPIModuleWithSettings an api that has the RAW serving the index.html, it freaked out. Maybe there is a way to handle that, but it’s not like that is probably what you want anyhow.

The myTypes Sum Type you want to add to for every type that you want to export over to purescript. frontEndRoot is where the generated files will go.

The Proxy business is a bunch of typelevel programming boilerplate. So is the empty MyBridge type.

There is basically no content to this code.

You also need to add this app/PSGenerator.hs file to your cabal file.

executable psGenerator
  hs-source-dirs:      app
  main-is:             PSGenerator.hs
  other-modules:       Lib
  -- Other library packages from which modules are imported.
  build-depends:       base >=4.8 && < 6.0
                     , aeson
                     , containers
                     , filepath
                     , ghc-mod
                     , http-api-data
                     , http-types
                     , lens
                     , mainland-pretty
                     , purescript-bridge
                     , servant
                     , servant-foreign
                     , servant-purescript
                     , servant-subscriber
                     , text
                     , servant-server
                     , wai
                     , warp
                     , bytestring

  -- Directories containing source files.
  hs-source-dirs:      src

  -- Base language which the package is written in.
  default-language:    Haskell2010

 

Every time you want to run the generator, you need to run

stack exec psGenerator

 

This then will put an API file and a Data type file into your purescript source in frontend/src

Using the API is a touch annoying but correct. If you look at the generated signature

getUsers :: forall eff m.
            MonadAsk (SPSettings_ SPParams_) m => MonadError AjaxError m => MonadAff ( ajax :: AJAX | eff) m
            => m (Array User)

There are a lot of constraints you need to satisfy in the monad m in order to call this thing. You need a monad that is Reader-like for getting the SPSettings_, needs to handle a Possible AjaxError, and needs to be an Aff-like monad. Woof.

It makes sense that you’d want to do all of this, but it is a burdensome mental overhead to get started.

Here’s some very basic source that shows how to at least get to the stage where you can log it the resulting request. I’m just dumping the error like a bad boy.

module Main where
import Prelude


import Control.Monad.Aff (Aff)
import Control.Monad.Aff.Console
import Control.Monad.Trans.Class
import Data.Maybe
import Control.Monad.Eff.Console (CONSOLE)

import ServerAPI
import Lib (User(..), _User)

import Control.Monad.Aff
import Control.Monad.Eff.Class
import Data.Either
import Control.Monad.Reader.Trans
import Control.Monad.Except.Trans
import Control.Monad.Eff.Exception (EXCEPTION)
import Network.HTTP.Affjax (AJAX, get)

import Servant.PureScript.Affjax
import Servant.PureScript.Settings

import Data.Array ((!!))
import Unsafe.Coerce 

import Data.Lens
import Data.Symbol (SProxy(..))
import Data.Lens.Record (prop)
import Data.Traversable


settings = defaultSettings $ SPParams_ { baseURL : "http://localhost:9000/" }



type MySettings = SPSettings_ SPParams_
type APIEffect eff = ReaderT MySettings (ExceptT AjaxError (Aff ( ajax :: AJAX, err :: EXCEPTION  | eff)))



runEffect :: forall eff. MySettings -> APIEffect eff (Array User) -> Aff ( ajax :: AJAX, err :: EXCEPTION | eff) (Array User)
runEffect settings m = do
    er <- runExceptT $ runReaderT m settings
    case er of
      Left err -> pure $ []
      Right v -> pure v


getName :: User -> String
getName (User {name : n }) = n

name :: forall a b r. Lens { name :: a | r } { name :: b | r } a b
name = prop (SProxy :: SProxy "name")

main = launchAff do
          users <- runEffect settings getUsers
          log $ maybe "No name" (view $ _User <<< name) (users !! 1 )
          log $ (view $ traversed <<< _User <<< name) users

Note that you have to install purescript-servant-support as it tells you when you run psGenerator. I’ve been using psc-package. It is often helpful to go in to the psc-package.json file and update to the latest package-set. Just a little tip.

You see that the ExceptT handles the AjaxError and the ReaderT supplies the settings, which uses the defaults + a baseURL to point the request to

The whole thing is run inside an Aff monad.

 

Here’s the basic servant code

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lib
    ( startApp
    , app
    , userAPI
    , userAPI'
    , Hello
    , User
    ) where

--import Prelude ()
--import Prelude.Compat

--import Control.Monad.Except
--import Control.Monad.Reader
--import Data.Aeson.Compat
import Data.Aeson.Types
--import Data.Attoparsec.ByteString
import Data.ByteString (ByteString)
import Data.List
import Data.Maybe
--import Data.String.Conversions
--import Data.Time.Calendar
import GHC.Generics
--import Lucid
--import Network.HTTP.Media ((//), (/:))
import Network.Wai
import Network.Wai.Handler.Warp
import Servant
--import System.Directory
--import Text.Blaze
--import Text.Blaze.Html.Renderer.Utf8
import qualified Data.Aeson.Parser
--import qualified Text.Blaze.Html
import Data.Text  (Text)



data User = User
  { name :: String
  , age :: Int
  , email :: String
  } deriving (Eq, Show, Generic)

instance FromJSON User
instance ToJSON User

instance FromJSON Hello
instance ToJSON Hello

users1 :: [User]
users1 =
  [ User "Isaac Newton"    372 "isaac@newton.co.uk" 
  , User "Albert Einstein" 136 "ae@mc2.org"         
  ]

type UserAPI = "users" :> Get '[JSON] [User] 
type UserAPI1 = UserAPI :<|> Raw

server1 :: Server UserAPI1
server1 = return users1 :<|> serveDirectoryFileServer "./frontend"

userAPI :: Proxy UserAPI1
userAPI = Proxy

userAPI' :: Proxy UserAPI
userAPI' = Proxy

-- 'serve' comes from servant and hands you a WAI Application,
-- which you can think of as an "abstract" web application,
-- not yet a webserver.
app1 :: Application
app1 = serve userAPI server1



main :: IO ()
main = do putStrLn "on port 9000"
          run 9000 app1

startApp = main
app = app1

 

Again, I started using the stack servant template, whose directory structure I’m complying with.

 

Edit: Some more comments: Purescript bridge is a seperate project from servant-purescript. Purescript bridge will translate your Haskell types. Servant purescript writes your api calls. The two lines in the main of PSGenerator.hs do these sepearte tasks. the writeAPI writes the API calls and  writePSTypes writes the types.

If you want to transport a parametrized data type like (Maybe a) in the myTypes things, hand the type a special type from here

https://hackage.haskell.org/package/purescript-bridge-0.11.1.2/docs/Language-PureScript-Bridge-TypeParameters.html

works like a charm

 

 

Elm, Eikonal, and Sol LeWitt

We saw this cool Sol LeWitt wall at MASS MoCA. It did not escape our attention that it was basically an eikonal equation and that the weird junctures were caustic lines.

It was drawn with alternating colored marker lines appearing a cm away from the previous line. This is basically Huygens principal.

So I hacked together a demo in elm. Elm is a Haskell-ish language for the web.

 

 

 

So I made a quick rip and run elm program to do this. This is the output, which I could make more dynamic.

The algorithm is to turn a list of points into their connecting lines. Then move the line perpendicular to itself, then recompute the new intersection points. It’s somewhat reminiscent of Verlet integration. Lines coordinates are momentum-like and points are position like and we alternate them. This is a finite difference version of the geometric Huygen’s principle.

Alternative methods which might work better include the Fast Marching Method or just using the wave equation and then plotting iso surfaces.

I also had to resample the function to get only the maximum y value for each x value in order to duplicate the LeWitt effect.

sol

These are the helper functions with lots of junk in there

module LineHelpers exposing (..)
-- Maybe should just be doubles or nums

import Debug

fromJust : Maybe a -> a
fromJust x = case x of
    Just y -> y
    Nothing -> Debug.crash "error: fromJust Nothing"

toPointString : List (number, number) -> String
toPointString xs =
  case xs of
    (x,y) :: ys -> (toString x) ++ "," ++ (toString y) ++ " " ++ (toPointString ys)
    _ -> ""



crossProd : (number,number,number) -> (number,number,number) -> (number,number,number)
crossProd (a,b,c) (d,e,f) = (b * f - c * e, c * d - a * f, a * e - b * d)


type alias PointListH number = List (number,number,number)
type alias LineListH number = List (number,number,number)


-- gives the mapping function the list and the list shifted by 1
neighbormap f a = let a_ = fromJust (List.tail a) in List.map2 f a a_


crossNeighbor = neighbormap crossProd

norm a b = sqrt (a * a + b * b)
shiftLine delta (a,b,c)  = (a,b, (norm a b) * delta + c)

connectingLines = crossNeighbor
shiftLines delta = List.map (shiftLine delta)
intersections = crossNeighbor


-- nearly striaght lines will find their intersection at infinity.
-- maybe filter out a lower threshold on c
-- keep first and last point
last xs = let l = List.length xs in fromJust (List.head (List.drop (l - 1) xs))

timestep : Float -> List (Float,Float, Float) -> List (Float,Float, Float)
timestep delta points = let
        firstpoint = fromJust (List.head points)
        lastpoint = last points
        connectlines = connectingLines points
        newlines = shiftLines delta connectlines
        newpoints = intersections newlines
        filterednewpoints = List.filter (\(a,b,c) -> (abs c) > 0.01) newpoints
        normpoints = List.map normalize filterednewpoints
        result = firstpoint :: (normpoints ++ [lastpoint])
        resample = List.map (maxfunc (List.map dehomogenize result)) initx
        --result2 = removeoutoforder (-100000, 0,00) result
          in List.map homogenize (zip initx resample)


homogenize (a,b) = (a,b,1)
dehomogenize (a,b,c) = (a / c, b / c)
normalize = dehomogenize >> homogenize

zip = List.map2 (,)

initx = List.map (toFloat >>((*) 4.5)) (List.range -200 400)
--inity = List.map (\x -> x * x / 50) initx
--inity = List.map (\x -> 300 + x * x / -50) initx
--inity = List.map (\x -> 25 * sin (x / 20) + 250) initx
inity = List.map (\x -> 25 * sin (x / 20) + 250 + 15 * sin (x/13)) initx
initxy = zip initx inity
initxyh = List.map homogenize initxy


iterate n f x = if n == 0 then [] else (f x) :: iterate (n - 1) f (f x)

paths = (List.map << List.map) dehomogenize (iterate 60 (timestep 5.0) initxyh)

colors = List.concat (List.repeat (List.length paths) ["red", "blue", "yellow"] )

removeoutoforder prev xs = case xs of
          y :: ys -> if prev < y then (y :: removeoutoforder y ys) else removeoutoforder prev ys
          _ -> []

neighborzip a = let a_ = fromJust (List.tail a) in zip a a_
linearinterp x ((x1,y1), (x2,y2)) = (y1 * (x2 - x) + y2 * (x - x1)) / (x2 - x1)
maxfunc : List (Float, Float) -> Float -> Float
maxfunc points x = let
        pairs = neighborzip points

        filterfunc ((x1,y1), (x2,y2)) = (xor (x < x1) (x < x2))
        candidates = List.filter filterfunc pairs
        yvals = List.map (linearinterp x) candidates in Maybe.withDefault 100 (List.maximum yvals)

And this is the svg main program.

import Html exposing (Html, button, div, text)
import Html.Events exposing (onClick)
import Svg exposing (..)
import Svg.Attributes exposing (..)
import LineHelpers exposing (..)

roundRect : Html.Html msg
roundRect =
    svg
      [ width "1000", height "1000",viewBox "-100 0 350 350" ]
      (List.reverse ([--[ rect [ x "10", y "10", width "100", height "100", rx "15", ry "15" ] [],
      -- polyline [ fill "none", stroke "red", points "20,100 40,60 70,80 100,20" ] [],
       polyline [ fill "none", stroke "black", strokeWidth "5.0", points (LineHelpers.toPointString LineHelpers.initxy) ] []] ++
         (List.map2 (\path color -> polyline [ fill "none", stroke color, strokeWidth "3.0", points (LineHelpers.toPointString path)] []) LineHelpers.paths LineHelpers.colors)))




main =
  Html.beginnerProgram { model = model, view = view, update = update }


-- MODEL

type alias Model = Int

model : Model
model =
  0


-- UPDATE

type Msg = Increment | Decrement

update : Msg -> Model -> Model
update msg model =
  case msg of
    Increment ->
      model + 1

    Decrement ->
      model - 1


-- VIEW

view : Model -> Html Msg
view model =
  div []
    [ button [ onClick Decrement ] [ Html.text "-" ]
    , div [] [ Html.text (toString model) ]
    , button [ onClick Increment ] [ Html.text "+" ],
    roundRect
    ]

 

 

notes on elm

elm is installed with npm

elm-repl

you import packages (including your own) with

import ThisPackage

and you check types by just writing them and hitting enter rather than :t

elm-live is a very handy thing. A live reloading server that watches for changes in your files.

elm-make myfile.elm

will generate the javascript and html

This is a good tutorial and a good snippet to get you going

 

Differences from Haskell:

elm isn’t lazy which is probably good.

The composition operator (.) is now <<

elm doesn’t have the multiline pattern match of haskell. You need  to use case expressions. I miss them.

typeclass facilities are not emphasized.

The list type is List a rather than [a]

 

Contracts and Category Theory

Contracts are both less cryptic and less impressive than a type system.

A type system somehow proves that things will never happen at compile time. You’ll never get a string when you expected an int or even more powerful facts. Contracts just guarantee that at least if certain problems occur at least the program will freak out and tell you at runtime.

I had been vaguely aware of contracts which I considered to be kind of a band aid Racket thing that is their solution to type safety (besides typed racket), but I did not go into depth. And I kind of viewed the thing more as a methodology for showing loop invariants and algorithmic correctness rather than type correctness. I do not know if this is an accurate portrayal of what is in Racket and I’m pretty sure contracts do not actually originate there (Eiffel?).

Mike Stay (who you may know as the co-author of the Rosetta Stone paper https://arxiv.org/abs/0903.0340)made a bunch of videos which I don’t know how I didn’t come across before (they’re kind of old by skateboarding millennial mountain dew front end developer standards. Did Node even exist? Barely.). Javascript (well maybe after python) was my language of greatest comfort a couple years ago and I would have loved this. I absolutely loved Bartosz Milewski’s Category Theory for Programmer’s series. There is a crap-ton of line noise  that kind of muddies the waters though in javascript. I wonder if it makes sense to me because I mostly already understand what he’s going for from a Haskell context. He has some cool patterns here like using objects as typeclasses/interfaces.

https://jscategory.wordpress.com/

The really neat thing he discusses is higher order contracts which I’d bet is a central piece of contract based programming but I had never gotten that far.

I’m still skimming over the vids, but nice job.

 

Some simple ST Monad examples

The ST monad is what you use to do real mutable state in Haskell basically.

The State monad is a more pure guy that just automatically threads the state through pure functions for you.

The ST monad, and structures in it, to my understanding is actually backed by computer memory that is changing. Some things that should be fast and easy become actually fast and easy. Like changing a single element in an array without rebuilding the whole damn thing (or a lot of it).

The ST monad is probably bad style. You’re supposed to bend over backward to avoid mutability. It’s a gun. Don’t shoot yourself. Maybe better style is to use the C FFI (foreign function interface) if you really really need mutability.

Edit (2/4/19): Woah, I really don’t agree with the above anymore. You should turn to the ST monad WAY before the C FFI (and odds are you need neither). To suggest otherwise is insane. Although inline-c is an easy package to sprinkle in a little c.

Unlike the IO monad the ST monad can be escaped. Sometimes this is called thawing and freezing, the process of going into and out of the monad.

Here’s a couple snippets that demo how it works.

I recommend not thinking about the actual monad laws of this thing. The type signature of ST is messed up. It uses some kind of weird type argument to guarantee in the typechecker that the ST monad reference can’t leak outside the monad. In terms of just pretending the do notation is imperative like, it makes sense though.

makeSTRef puts that value you give it into the variable n.

readSTRef pulls out. Modify Let’s you modify.

runST ubiquitously has to be used to rip off the ST monad layer. You don’t want it if you want to combine a bunch of little ST functions. makeArray’ doesn’t have it so if you look at it in ghci you don’t see 10, you see <<ST Action>>. If you haven’t read the reference or frozen the vector, you can’t use runST. You’ll get an error because that would leak the mutable thing out of the monad.

Vectors are how Haskell has actual c style arrays. It’s kind of like numpy if you’re familiar with that. Unboxed means you’re using raw ints and floats and stuff.

M.replicate builds a size 3 vector filled with doubles of value 1.2. Then I modify the second element and freeze it into an immutable vector to escape the monad.

Storable vectors might be the better default. They are the same really, except they can be passed through the C FFI. I believe hmatrix uses them (and other c interfacing libraries) for passing arrays into Haskell.

import Control.Monad.ST
import Data.STRef
import Control.Monad
import Data.Vector.Unboxed.Mutable as M
import Data.Vector.Unboxed as V
 
 
sumST :: Num a => [a] -> a
sumST xs = runST $ do           -- runST takes out stateful code and makes it pure again.
 
    n <- newSTRef 0             -- Create an STRef (place in memory to store values)
 
    Control.Monad.forM_ xs $ \x -> do         -- For each element of xs ..
        modifySTRef n (+x)      -- add it to what we have in n.
 
    readSTRef n                 -- read the value of n, and return it.




makeArray = runST $ do
    n <- newSTRef [1,2,3]
    readSTRef n

makeArray' = newSTRef 10 >>= readSTRef

makeArray'' = do 
	a <- newSTRef 10 
	b <- newSTRef 11
	return (a,b) 



makeVec = runST $ do
	v <- M.replicate 3 (1.2::Double)
	write v 1 3.1
	V.freeze v