List.hs

{-# Language ConstraintKinds #-}
{-# Language DataKinds #-}
{-# Language DeriveFunctor #-}
{-# Language FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# Language InstanceSigs #-}
{-# Language MultiParamTypeClasses #-}
{-# Language OverloadedLabels #-}
{-# Language PatternSynonyms #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneDeriving #-}
{-# Language TemplateHaskell #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}
{-# Language ViewPatterns #-}

module List where

-- base
import           Data.Functor.Classes
import           GHC.TypeLits (Symbol)

-- recursion-schemes
import           Data.Functor.Foldable             hiding ( ListF(..) )

-- deriving-compat
import           Text.Show.Deriving                       (deriveShow1)

-- row-types
import           Data.Row
import           Data.Row.Internal
import           Data.Row.Variants                        ( view
                                                          , unsafeInjectFront
                                                          , unsafeMakeVar)

-- Apply a type to a row of (* -> *)
type family ApplyRow x (r :: Row (* -> *)) :: Row * where
  ApplyRow x ('R lt) = 'R (ApplyLT x lt)

type family ApplyLT x (r :: [LT (* -> *)]) :: [LT *] where
  ApplyLT _ '[] = '[]
  ApplyLT x (l :-> f ': fs) = ((l :-> f x) ': ApplyLT x fs)

-- A newtype that wraps a variant. The variant is a row made up of (* -> *)
-- that are all given the same type.
newtype VarWrapF (r :: Row (* -> *)) x = VarWrapF {unVarF :: Var (ApplyRow x r)}
deriving instance (Eq (Var (ApplyRow x r))) => Eq (VarWrapF r x)
deriving instance (Show (Var (ApplyRow x r))) => Show (VarWrapF r x)

instance Functor (VarWrapF ('R '[])) where
  fmap = error "impossible"

-- Since all possible elements of the wrapped variant were given the same
-- type, we can map over any of them.
instance ( KnownSymbol l
         , Functor f
         , s ~ 'R fs, Functor (VarWrapF s)
         , r ~ 'R (l ':-> f ': fs)
         ) => Functor (VarWrapF ('R (l :-> f ': fs))) where
  fmap :: forall a b. (a -> b) -> VarWrapF r a -> VarWrapF r b
  fmap f (VarWrapF v) = case trial v (Label :: Label l) of
    Left x -> VarWrapF (unsafeMakeVar (Label :: Label l) (fmap f x))
    Right v' ->
      let VarWrapF v'' = (fmap :: (a -> b) -> VarWrapF s a -> VarWrapF s b)
                            f (VarWrapF v')
      -- The compiler seemed very confused about what the type of fmap should be
      in VarWrapF (unsafeInjectFront v'')

instance Show1 (VarWrapF ('R '[])) where
  liftShowsPrec _ _ _ _ = undefined

instance ( KnownSymbol l, Show1 f, Show1 (VarWrapF ('R fs))
         ) => Show1 (VarWrapF ('R (l :-> f ': fs))) where
  liftShowsPrec sa x p (VarWrapF v) = case trial v (Label :: Label l) of
    Left fa -> showParen (p > 10) $
      showString "VarWrapF " . liftShowsPrec sa x p fa
    Right v' -> liftShowsPrec sa x p (VarWrapF @('R fs) v')

-- Use Fix to obtain a recursive structure.
type VarWrap r = Fix (VarWrapF r)

-- Constraint synonym for patterns
type GenericPattern l f v r = (ApplyRow v r .! l ≈ f v, AllUniqueLabels (ApplyRow v r))

-------------- Example --------------

-- We create three different data types corresponding to three constructors
-- of a variant. Patterns are polymorphic over the row.

data ConsF a x = ConsF' a x
  deriving (Eq, Functor, Show)
$(deriveShow1 ''ConsF)

pattern ConsF :: ( GenericPattern "consF" (ConsF a) v r
                 ) => a -> v -> VarWrapF r v
pattern ConsF a v <- VarWrapF (view #consF -> Just (ConsF' a v)) where
        ConsF a v = VarWrapF (IsJust (Label :: Label "consF") (ConsF' a v))

pattern Cons a v = Fix (ConsF a v)

data Cons2F a x = Cons2F' a a x
  deriving (Eq, Functor, Show)
$(deriveShow1 ''Cons2F)

pattern Cons2F :: ( GenericPattern "cons2F" (Cons2F a) v r
                  ) => a -> a -> v -> VarWrapF r v
pattern Cons2F a b v <- VarWrapF (view #cons2F -> Just (Cons2F' a b v)) where
        Cons2F a b v = VarWrapF (IsJust (Label :: Label "cons2F") (Cons2F' a b v))

pattern Cons2 a a' v = Fix (Cons2F a a' v)

data NilF x = NilF'
  deriving (Eq, Functor, Show)
$(deriveShow1 ''NilF)

pattern NilF :: ( GenericPattern "nilF" NilF v r
                ) => VarWrapF r v
pattern NilF <- VarWrapF (view #nilF -> Just NilF') where
        NilF = VarWrapF (IsJust (Label :: Label "nilF") NilF')

pattern Nil = Fix NilF

-- Two example list types. Both use the same Nil and Cons types.
type ListRowF a = ("consF" .== ConsF a .+ "nilF" .== NilF)
type ListF a x = VarWrapF (ListRowF a) x
type List a = Fix (VarWrapF (ListRowF a))

type List2RowF a =
  ("consF" .== ConsF a .+ "nilF" .== NilF .+ "cons2F" .== Cons2F a)
type List2F a x = VarWrapF (List2RowF a) x
type List2 a = Fix (VarWrapF (List2RowF a))

-- Define a generic operation that maps the a's of a constructor to b's
class OverList (f :: * -> *) r a b where
  overList' :: (a -> b) -> f (VarWrap r) -> VarWrap r

-- Boilerplate instance
instance OverList (VarWrapF ('R '[])) r a b where
  overList' _ _ = error "Impossible"

-- Boilerplate instance
instance ( KnownSymbol l
         , OverList f r a b
         , s ~ 'R fs
         , OverList (VarWrapF s) r a b
         ) => OverList (VarWrapF ('R (l ':-> f ': fs))) r a b where
  overList' f (VarWrapF x) = case trial x (Label :: Label l) of
    Left x -> overList' f x
    Right xs -> (overList' :: (a -> b) -> VarWrapF s (VarWrap r) -> VarWrap r) f (VarWrapF xs)

instance ( v ~ VarWrap r
         , AllUniqueLabels (ApplyRow v r)
         , ApplyRow v r .! "nilF" ≈ NilF v
         ) => OverList NilF r a b where
  overList' _ NilF' = Nil

instance ( v ~ VarWrap r
         , AllUniqueLabels (ApplyRow v r)
         , ApplyRow v r .! "consF" ≈ ConsF b v
         ) => OverList (ConsF a) r a b where
  overList' f (ConsF' a x) = Cons (f a) x

-- This function will transform one VarWrap type to another as long as all
-- constructors in r implement OverList. Since OverList is implemented for NilF
-- and ConsF, overList can be used on List's but not List2's
overList :: ( Functor (VarWrapF r)
            , OverList (VarWrapF r) r' a b
            ) => (a -> b) -> VarWrap r -> VarWrap r'
overList f = cata (overList' f)

main :: IO ()
main = do
  -- Cons and Nil can be used in different types
  let l1 = Cons 0 (Cons 1 Nil) :: List Int
      l2 = Cons2 2 3 (Cons 4 Nil) :: List2 Int

  print l1
  -- > Fix (VarWrapF (ConsF' 0 (Fix (VarWrapF (ConsF' 1 (Fix (VarWrapF NilF')))))))

  print l2
  -- > Fix (VarWrapF (Cons2F' 2 3 (Fix (VarWrapF (ConsF' 4 (Fix (VarWrapF NilF')))))))

  -- We can use recursion schemes over the structures to change them. In this
  -- example, a List is changed to a List2
  let l3 = cata ( Fix
                . VarWrapF
                . diversify @("cons2F" .== Cons2F Int (List2 Int))
                . unVarF)
             l1 :: List2 Int
  print l3
  -- > Fix (VarWrapF (ConsF' 0 (Fix (VarWrapF (ConsF' 1 (Fix (VarWrapF NilF')))))))

  print (overList (+(1::Int)) l1 :: List Int)
  -- > Fix (VarWrapF (ConsF' 1 (Fix (VarWrapF (ConsF' 2 (Fix (VarWrapF NilF')))))))