MapRecord for PureScript, with and without comments!

MapRecord.purs

module MapRecordWithComments where

-- | Type-level Tomfoolery. A million thankyous to @kcsongor and his
-- | unparallelled patience with me while I try to figure this stuff
-- | out.

import Prelude (($), (+), (<>), discard, show)

import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (CONSOLE, log)
import Data.Record (insert, delete, get)
import Data.Symbol (SProxy(..), class IsSymbol)
import Data.Unit (Unit)
import Global.Unsafe (unsafeStringify)
import Type.Row (class RowLacks, class RowToList, Cons)

-- | Here's a question: we know we can map over _arrays_ with relative
-- | ease, but what about objects? They don't really make sense as a
-- | functor, but what if we want to scale coordinates? Or capitalise
-- | a dictionary of owners' pets' names? We can write some ugly stuff
-- | to do it, but there will be a _lot_ of boilerplate. Wouldn't it
-- | be great if we could say, as long as all the values have the same
-- | type, we can apply `f` to all values?

---

-- | This is a scary beasty, so let's break it down. `Type` is, as you
-- | may have guessed, a type. We could substitute `Int` and `String`
-- | for `a` and `b`, for example, and no trouble would come of it.

-- | The possibly scary bits are the `# Type` fields. This represent
-- | rows of types. For example, `Eff :: # Effect -> Type -> Type` -
-- | we give it an "effect row", then a return type, and that gives us
-- | a `Type` for our functions! Anyway, it turns out that, behind the
-- | scenes, `{ a: 1, b: 2 }` is actually represented with a `Record`:
-- | `Record (a :: Int, b :: Int)`. Wouldn't you know it, there's our
-- | row type! `ra` and `rb` are therefore going to be the row type in
-- | some `Record` we're interested in.

-- | The other interesting thing here is the functional dependencies,
-- | or "fundeps". What these say is that, given the types `ra` and
-- | `b`, you can always know the type of `rb`. Similarly, given `rb`
-- | and `a`, you can always know the type of `ra`.

-- | What these _actually_ represent are the two stages of our "map".
-- | `ra` is the row of input, `a` is the type of its fields. The same
-- | is true for `b`. Because we apply a single function to a row of
-- | the same type, if we have that input row and an output type, we
-- | can work out the whole of the output's type: it'll have the keys
-- | of the input row, all of which will have the type of the output.
-- | Similarly, the input will have the keys of the output, and the
-- | type of the input. That's how to read those two dependencies!
class MapRecord
  (ra :: # Type)
  (rb :: # Type)
  ( a ::   Type)
  ( b ::   Type)
  | ra b -> rb
  , rb a -> ra
  where

    -- | This is the sweet, harmless front on top of all the machinery
    -- | that we'll build. If you can give me `a -> b` and a record of
    -- | `ra`, I'll give you `rb`. How do we know the types will line
    -- | up? Our functional dependencies make sure of it. We'll see in
    -- | a second how this gets expressed. Note that `ra -> a` (and
    -- | `rb -> b`) sounds like a good candidate at first - if we have
    -- | the whole row, the single type can be found by looking at any
    -- | of its occupants, right? This is fine as long as your row is
    -- | inhabited... I discovered this when I tried an empty row!
    mapRecord :: (a -> b) -> Record ra -> Record rb

-- | For an empty record, our work here is pretty straightforward. We
-- | just return another empty record - after all, we mapped over all
-- | its inhabitants, right?

-- | The name is prefixed with `_` because, until we get cool stuff
-- | like instance chains, there's no explicit way to give a priority
-- | of instances; the compiler simply goes in alphabetical order. Our
-- | _other_ instance, unfortunately, is general enough to pick up all
-- | the `Nil` instances, so we have to look at this one first. We do
-- | have a couple options available, one of which involves passing
-- | around the `RowList` type so we can pattern match for `Cons` and
-- | `Nil`*. However, that complicates this code, so feel free to look
-- | at the link at the bottom, or ignore the "Overlapping instances"
-- | error that your compiler will give you. We know what we're doing
-- | with this... I think!
instance _mapRecordNil :: MapRecord () () a b where
  mapRecord _ {} = {}

-- | OK, let's look at this terror. We have tons of constraints here,
-- | so we'll try to go through them one by one. Basically, we use the
-- | `RowToList` to get a `k` (key) out of our object that we can use.
-- | Then, we define the row "tails" in terms of `ra` and `k`, require
-- | that the _tail_ can `MapRecord`, and then we're good. How do we
-- | know? Well, `k` lets us check that the same type is in the same
-- | key for both records.
instance mapRecordCons
    :: ( -- K, whatever it is, is some kind of "Symbol": the kind of
         -- strings at the type-level. We use this for record access!
         IsSymbol k

         -- Here, we introduce `(Cons k a la)`, the `List` form of the
         -- `ra` row. In a sense, we say that `ra` is defined as one
         -- `a` value, indexed by `k`, and a list of other key/value
         -- sets, `la`. Now, the compiler can find a value for `k`!
       , RowToList ra (Cons k a la)

         -- What do we call `ra` when it's missing a `k` of type `a`?
         -- `ta`. Like the *tail* of the *record* of `a`.
       , RowCons k a ta ra

         -- For the compiler's peace of mind, we can assert here that,
         -- if `ta` is `ra` without the `k` value, then the `ta` row
         -- definitely lacks a `k` value. The compiler isn't sentient
         -- just yet :)
       , RowLacks k ta

         -- While we're at it, we can do the same two things for `rb`.
       , RowCons k b tb rb
       , RowLacks k tb

         -- Here's the "recursion". When we used `RowCons`, not only
         -- did we get `k`, but we also got `a` and `b`. We can now
         -- "pass these down" to the rest of the record to make sure
         -- that all the fields have the same types. Because our type-
         -- class requires an `a -> b`, and we know all our types are
         -- `a` in the input and `b` in the output, and that all the
         -- keys are the same... well, there can't be many things we
         -- could possibly be doing, right?
       , MapRecord ta tb a b
       )

       -- Given aaaall that evidence, this seems pretty clear. If this
       -- is true for the record without a `k` value, for any `k` that
       -- you like, and the heads are type `a` and `b`, we can be sure
       -- that we have a mappable record.
    => MapRecord ra rb a b
  where
    -- | Do the actual mapping. Almost forgot about this bit!
    mapRecord f row =
      let
        -- `k` is the type-level name of our chosen field. So, we can
        -- use that in this signature to have a "value-level proxy" of
        -- the data at the type-level. This is some dependent type
        -- wizardry now.
        name :: SProxy k
        name = SProxy

        -- Now we have a `Symbol` for our property, this bit is really
        -- quite easy: get the value at that name. What's its type? No
        -- surprises there!
        head :: a
        head = get name row

        -- We now have to _remove_ that item, and then `mapRecord` on
        -- the rest, just like we would if we were doing recursion on
        -- a list.
        tail :: Record tb
        tail = mapRecord f (delete name row)

         -- Take our freshly-transformed tail, and insert the value of
         -- the transformed head at the `k` index. All that type stuff
         -- for one simple line of code...
      in insert name (f head) tail

---

-- | With all that behind us, let's see some examples!
main :: Eff (console :: CONSOLE) Unit
main = do
  log $ unsafeStringify $ empty
  log $ unsafeStringify $ addition
  log $ unsafeStringify $ string
  where

    -- Pretty boring, but we _do_ have to give a type for our non-
    -- existent keys in order for the compiler to print it! We can
    -- replace `Int` with any `Show`able type, and this will work.
    empty :: {}
    empty = mapRecord (show :: Int -> String) {}

    -- Do some maths at every position. You might want to try changing
    -- one of the types in this record - you'll get a type error! At
    -- compile time! I don't think we're in JavaScript anymore, Toto!
    addition :: { a :: Int
                , b :: Int
                , c :: Int
                }
    addition = mapRecord (_ + 2)
      { a: 1010
      , b: 123
      , c: 0
      }

    -- The type system is yours to abuse. WWBD?
    string :: { freedom    :: String
              , equality   :: String
              , fraternity :: String
              }
    string = mapRecord (_ <> "é")
      { freedom:    "Libert"
      , equality:   "Égalit"
      , fraternity: "Beyonc"
      }

-- | * https://github.com/justinwoo/purescript-map-record/blob/master/src/Main.purs#L18

MapRecordWithoutComments.purs

module MapRecord where

import Data.Record (insert, delete, get)
import Data.Symbol (SProxy(..), class IsSymbol)
import Type.Row (class RowLacks, class RowToList, Cons)

class MapRecord
  (ra :: # Type)
  (rb :: # Type)
  ( a ::   Type)
  ( b ::   Type)
  | ra b -> rb
  , rb a -> ra
  where
    mapRecord :: (a -> b) -> Record ra -> Record rb

instance _mapRecordNil :: MapRecord () () a b where
  mapRecord _ {} = {}

instance mapRecordCons
    :: ( IsSymbol k
       , RowToList ra (Cons k a la)
       , RowCons k a ta ra
       , RowLacks k ta
       , RowCons k b tb rb
       , RowLacks k tb
       , MapRecord ta tb a b
       )
    => MapRecord ra rb a b
  where
    mapRecord f row =
      let
        name :: SProxy k
        name = SProxy

        head :: a
        head = get name row

        tail :: Record tb
        tail = mapRecord f (delete name row)

      in insert name (f head) tail