Spacefinder.purs

module Main where
--------------------------------------------------------------------------------
import Data.HeytingAlgebra
import Prelude

import Data.Array (filter, any, (:), uncons)
import Data.Either (Either(..))
import Data.Maybe (Maybe(..))
import Data.Profunctor (class Profunctor, arr)
import Data.Profunctor.Choice (class Choice, left)
import Data.Profunctor.Strong (class Strong, first, (&&&))
import Data.Tuple (Tuple(..), fst, snd, swap, uncurry)
--------------------------------------------------------------------------------

-- | Toy definition for elements in the DOM
newtype Element = Element { tagName ∷ String, top ∷ Int }

-- | This is the equivalent of Element.toString
instance elShow ∷ Show Element where
  show (Element { tagName, top }) = "(" <> tagName <> "," <> (show top) <> "px)"

elements :: Array Element
elements = [ Element { tagName: "h2", top: 0 }
           , Element { tagName: "p", top: 100 }
           , Element { tagName: "p", top: 300 }
           , Element { tagName: "h2", top: 350 }
           , Element { tagName: "p", top: 600 }
           , Element { tagName: "p", top: 900 }
           , Element { tagName: "p", top: 1200 }
           , Element { tagName: "p", top: 1600 }
           , Element { tagName: "div", top: 2000 }
           , Element { tagName: "p", top: 2300 }
           ]

-- | Asserts the type of an element
is ∷ String → Element → Boolean
is tn (Element { tagName }) = tn == tagName

-- | Asserts the position of an element from the top
fromTop ∷ Int → Element → Boolean
fromTop n (Element { top }) = n <= top

-- The combinators above are fine for simple predicates such as those
-- used by the `filter` function, and we can already combine them by
-- relying on the fact that predicates combine just like booleans do:
--
-- > :t is "div" && fromTop 500
-- Element -> Boolean
-- > filter (is "div" && fromTop 500) elements
-- [(div,2000px)]
--
-- In a typical language, you would have to manually create an anonymous
-- function but here it is done for us by the fact that && is defined in
-- a typeclass (`HeytingAlgebra`) and there is an instance of that class
-- for predicates:
--
-- instance heytingPred :: HeytingAlgebra b => HeytingAlgebra (a -> b) where
--   ...
--   conj f g a = f a && g a
--
-- However, that is not enough. The spacefinder needs to verify more complex
-- predicates that involve comparing elements between each other, e.g. "is there
-- an h2 300px above me?". You couldn't do that with filter, at least not without
-- free variables in your predicate that rely on the surrounding environment.
-- That is not a good way to write functions; we want anyone who's new to the
-- code to just understand it by looking at the type signatures.
--
-- One possible interpretation of that problem is to use state transformers, a
-- fancy name for a trivial concept:
--        state + input value produces updated state + output value

-- Let's create a data type, that will come in handy soon:
newtype StateTrans s i o = ST (Tuple s i → Tuple s o)

-- Right off the bat, let's write a utility function that will just call
-- a state transformer with initial state and input:
runState ∷ ∀ s i o. StateTrans s i o → s → i → Tuple s o
runState (ST st) s i = st (Tuple s i)

-- and do the same with an array of inputs by threading the output state
-- throughout:
iterateState ∷ ∀ s i o. StateTrans s i o → s → Array i → Tuple s (Array o)
iterateState st @ (ST f) s is
  | Just { head, tail } ← uncons is = let (Tuple s' o) = f (Tuple s head)
                                          (Tuple s'' os) = iterateState st s' tail
                                      in Tuple s'' (o : os)
  | otherwise                       = Tuple s []

-- If we choose our state type `s` wisely, we can express all kinds of
-- predicates. Alas, we have lost the nice and clean DSL of boolean expressions.
-- Can we get it back? Yes we can! Functions `a -> b` are just one example of
-- morphisms `f` mapping objects to objects. That notion is defined by the
-- `Category` type class, of which (->) has an instance.
--
-- If we can write an instance of `HeytingAlgebra` for categories, and make
-- our `StateTrans` a category, then we can have our cake and eat it too!
-- Sadly, `Category` is too generic: we wouldn't even know how to call or
-- even produce one value of "it". We need more help, and that help will come
-- from strong profunctors. A type `f` that is a strong profunctor allows us to
--   1- lift any function `a -> b` into a functor `f a b` using `arr`
--   2- work on product types by turning an `f a b` and an `f c d` into an
--      `f (Tuple a c) (Tuple b d)`
--
-- More details are available on Pursuit.
-- 
-- Let's start with defining our `HeytingAlgebra` first:

-- Wrap a bifunctor so we can define non-orphan instances
-- (that is a PureScript limitation)
newtype F f a b = F (f a b)

instance fHeyting ∷ (HeytingAlgebra b, Category f, Strong f) ⇒ HeytingAlgebra (F f a b) where
  ff = F $ arr $ const ff
  tt = F $ arr $ const tt
  implies (F f) (F g) = F $ arr (uncurry implies) <<< (f &&& g)
  conj (F f) (F g) = F $ arr (uncurry conj) <<< (f &&& g)
  disj (F f) (F g) = F $ arr (uncurry disj) <<< (f &&& g)
  not (F f) = F $ arr not <<< f

-- That was easy and fairly mechanical. As usual with polymorphic functions,
-- there usually is only one possible implementation (modulo coding style).

-- Let's now turn our state transformer, first into a category:

instance stSemigroupoid ∷ Semigroupoid (StateTrans s) where
  compose ∷ ∀ a b c. StateTrans s b c → StateTrans s a b → StateTrans s a c
  compose (ST sbc) (ST sab) = ST $ sbc <<< sab

instance stCategory ∷ Category (StateTrans s) where
  id ∷ ∀ a. StateTrans s a a
  id = ST id

-- ... second into strong profunctors

instance stFunctor ∷ Functor (StateTrans s a) where
  map f (ST g) = ST $ second f <<< g

instance stProfunctor ∷ Profunctor (StateTrans s) where
  dimap f g (ST st) = ST $ second g <<< st <<< second f

instance stStrong ∷ Strong (StateTrans s) where
  -- I offer a dring to the first one who figures that one out
  -- (check the previous revision for a clearer version, this
  -- one was for personal musing)
  first (ST f) = ST $ ((fst <<< fst) &&& (snd *** id)) <<< first f <<< ((id *** fst) &&& (snd <<< snd))
  second f = arr swap <<< first f <<< arr swap

-- Done. It is worth noting that none of the above has anything to do with
-- spacefinder; it can be put in its own module and specialised in as many
-- contexts as we wish. There is a whole family of profunctors too, and it
-- is possible to write instances for state transformers for several of them.

-- Now we can finally define the spacefinder. We choose our state to be the
-- array of elements, each with an accompanying boolean to track whether it
-- is a valid hole or not.
type State = Array (Tuple Element Boolean)
type Spacefinder = F (StateTrans State) Boolean Boolean

-- Let's define a utility to run a spacefinder
runSpacefinder ∷ Spacefinder → Array Element → Array Element
runSpacefinder (F s) es = 
  let es' = es <#> (flip Tuple $ true)
      (Tuple es'' _) = runState s es' true 
  in map fst $ filter snd es''

-- | Lift any predicate acting on a single element into a Spacefinder
-- | We take the approach that the result will be false if all elements
-- | in the array failed
lift ∷ (Element → Boolean) → Spacefinder
lift f = F $ ST \(Tuple es b) →
  if b
  then let es' = map (\(Tuple e b) → Tuple e (b && f e)) es in Tuple es' (any snd es')
  else Tuple es false

-- | Here is an example of a spacefinder predicate that accepts elements
-- | only if they are `n + 1` elements away from the previous matching 
-- | element. Internally, we use a state transformer to keep track of the
-- | number of elements since the last matching one.
sepBy ∷ Int → Spacefinder
sepBy n = F $ ST $ \(Tuple es b) →
  if b
    then let (Tuple _ es') = iterateState check n es in Tuple es' (any snd es')
    else Tuple es false
  where
  check ∷ StateTrans Int (Tuple Element Boolean) (Tuple Element Boolean)
  check = ST f
    where
    f (Tuple n' (Tuple e b)) | b && n' >= n = Tuple 0 (Tuple e true)
                             | otherwise    = Tuple (n' + 1) (Tuple e false)