IApplicativeQuestionMark.hs

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds      #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE TypeOperators  #-}

-- For the "Another take"
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall #-}

import Data.Type.Nat
import Data.Proxy
import qualified Data.Vec.Lazy as V

-------------------------------------------------------------------------------
-- From the paper:
-------------------------------------------------------------------------------
type s :-> t = forall i. s i -> t i

class IFunctor f where
    imap :: (s :-> t)  -> f s :-> f t

data Path :: ((k,k) -> *) -> (k,k) -> * where
    Stop  ::                                Path g '(i, i)
    (:-:) :: g '(i, j) -> Path g '(j, k) -> Path g '(i, k)

instance IFunctor Path where
    imap _ Stop       = Stop
    imap f (r :-: rs) = f r :-: imap f rs

class IFunctor m => IMonad (m :: (k -> *) -> k -> *) where
    iskip   :: p :-> m p
    iextend :: (p :-> m q) -> (m p :-> m q)

-------------------------------------------------------------------------------
-- IMonad Path
-------------------------------------------------------------------------------

pathAppend :: Path g '(i, j) -> Path g '(j, k) -> Path g '(i, k)
pathAppend Stop       q = q
pathAppend (r :-: rs) q = r :-: pathAppend rs q

instance IMonad Path where
    iskip _x = undefined -- x :-: Stop -- cannot write, as GHC is silly :/

    iextend _ Stop = Stop
    iextend f (r :-: rs) = pathAppend  (f r) (iextend f rs)

ijoin :: IMonad m => m (m p) :-> m p
ijoin = iextend id

-------------------------------------------------------------------------------
-- IApplicative Path?
-------------------------------------------------------------------------------

data (:=) :: * -> k -> k -> * where
    V :: (:=) a i i

-- List is simple, basically no index
type List a = Path (a := '((), ()))

-- But what about Vec?
--
--     type Vec n a = Path ?
--
-- After wandering around, you'll end up with:
--
data Succ :: * -> (Nat, Nat) -> * where
    Succ :: a -> Succ a '(n, 'S n)

type Vec a n = forall p. Path (Succ a) '(p, Plus n p)

-- So what about Applicatives?
-- Well...
--
--     data Unit a = Unit
--     data (:*:) f g a = f a :*: g a
--
-- aren't good enough.

type Atkey m i j a = m (a := j) i

-- won't work for Path as Vec

-- We have to write specific variant for :*

class IApplicativePlus m where
    ipure :: x -> m (Succ x) '(n, 'S n)

    -- iprod omitted - I haven't tried, it's not that easy exercise.

instance IApplicativePlus Path where
    ipure x = Succ x :-: Stop

-- So what does this means?
--
-- We have
--
--     Vec :: * -> Nat -> *
--
-- If we a monoidal product of them, having something like
--
--     p = (x :: Vec a n, y :: Vec a m)  -- monoidal product is (,)
--
-- We want to multiply (pun unintended) the components so we get
--
--     xy = Vec a (Mult n m)             -- monoidal product is Mult
--
-- And the latter product is specific to each instance.
-- There's an IApplicative for ZipList applicative for Vec, but
-- there product is boring. Also there is a Plus(-like) monoidal "product"

-------------------------------------------------------------------------------
-- Conclusion
-------------------------------------------------------------------------------

-- So the `indexed` approach is to take common input-output things like Path
-- and split the pair into two argument:
--
-- Without an @a@ index, Path' is a Category...
data Path' f i o a where
    Nil   :: Path' f i i a
    (:>>) :: f x y a -> Path' f y z a -> Path' f x z a

data Succ' i o a where
    Succ' :: a -> Succ' n ('S n) a

type Vec' n a = forall m. Path' Succ' m (Plus m n)
-- and then life is easier. 

-------------------------------------------------------------------------------
-- Another take
-------------------------------------------------------------------------------

-- This is awful.

class IApp z p f | f -> z p where
    iunit :: a -> f z a
    iprod :: p n m q => f n a -> f m b -> f q (a, b)

class Mult n m ~ q => CMult n m q | n m -> q
instance CMult 'Z n 'Z
instance (CMult n m nm, Plus m nm ~ q) => CMult ('S n) m q

data Dict c where
    Dict :: c => Dict c

-- Vec is used as singleton
conjure :: V.Vec n a -> Proxy m -> Dict (CMult n m (Mult n m))
conjure V.VNil _ = Dict
conjure (_ V.::: xs) p = case conjure xs p of
    Dict -> Dict

instance IApp Nat1 CMult V.Vec where
    iunit x = x V.::: V.VNil
    iprod V.VNil       _  = V.VNil
    iprod (x V.::: xs) ys = iprod' (conjure xs Proxy) x xs ys where
        iprod' :: Dict (CMult n m q) -> a -> V.Vec n a -> V.Vec m b -> V.Vec (Plus m q) (a, b)
        iprod' Dict x xs ys = fmap ((,) x) ys V.++ iprod xs ys

-- >>> example
-- (True,'x') ::: (True,'y') ::: (True,'z') ::: (False,'x') ::: (False,'y') ::: (False,'z') ::: VNil
example :: V.Vec Nat6 (Bool, Char)
example = iprod as bs where
    as :: V.Vec Nat2 Bool
    as = True V.::: False V.::: V.VNil

    bs :: V.Vec Nat3 Char
    bs = 'x' V.::: 'y' V.::: 'z' V.::: V.VNil