headt.purs

module HEADT where

import Prelude

import Control.Alternative (class Alt, class Alternative, class Plus, empty, (<|>))
import Control.MonadZero (guard)
import Data.Either (Either(..))
import Data.Eq (class Eq1, eq1)
import Data.Identity (Identity(..))
import Data.Leibniz (type (~), coerceSymm)
import Data.Newtype (class Newtype, unwrap, wrap)
import Data.Ord (class Ord1, compare1)
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
import Partial.Unsafe (unsafeCrashWith)
import Prim.Row as R
import Prim.RowList as RL
import Record.Unsafe (unsafeGet, unsafeHas)
import Type.Equality (class TypeEquals)
import Unsafe.Coerce (unsafeCoerce)

type RowApply (f ∷ # Type -> # Type) (a ∷ # Type) = f a
infixr 0 type RowApply as +

data HProxy (h ∷ (Type -> Type) -> Type -> Type) = HProxy

class HVariantFMatchCases (rl :: RL.RowList) (vo :: # Type) (a :: Type -> Type) b | rl -> vo a b

instance hvariantFMatchCons 
  :: (HVariantFMatchCases rl vo' a b, R.Cons sym (HProxy h) vo' vo, TypeEquals k (h a b -> c)) 
  => HVariantFMatchCases (RL.Cons sym k rl) vo a b

instance hvariantFMatchNil :: HVariantFMatchCases RL.Nil () a b

newtype HVariantFRep h t a = HVariantFRep
  { type :: String
  , value :: h t a
  , hmap :: forall f g. (f ~> g) -> (h f ~> h g)
  }

data HVariantF (r :: # Type) (f :: Type -> Type) a

instance hfunctorHVariantF ∷ HFunctor (HVariantF r) where
  hmap :: forall f g. (f ~> g) -> HVariantF r f ~> HVariantF r g
  hmap g a = case coerceY a of
    HVariantFRep v -> coerceV $ HVariantFRep
      { type : v.type
      , value: v.hmap g v.value
      , hmap: v.hmap
      }
    where
      coerceY ∷ forall h f. HVariantF r f ~> HVariantFRep h f
      coerceY = unsafeCoerce
      coerceV ∷ forall h f. HVariantFRep h f ~> HVariantF r f
      coerceV = unsafeCoerce

injF
  ∷ forall sym h f r1 r2
  . R.Cons sym (HProxy h) r1 r2
  => IsSymbol sym
  => HFunctor h
  => SProxy sym
  -> h f
  ~> HVariantF r2 f
injF p value = coerceV $ HVariantFRep { type: reflectSymbol p, value, hmap }
  where
  coerceV ∷ HVariantFRep h f ~> HVariantF r2 f
  coerceV = unsafeCoerce

prjF
  ∷ forall sym h f g a r1 r2
  . R.Cons sym (HProxy h) r1 r2
  => Alternative g
  => IsSymbol sym
  => SProxy sym
  -> HVariantF r2 f a
  -> g (h f a)
prjF p = onF p pure (const empty)

onF
  ∷ forall sym h f c a r1 r2
  . R.Cons sym (HProxy h) r1 r2
  => IsSymbol sym
  => SProxy sym
  -> (h f a -> c)
  -> (HVariantF r1 f a -> c)
  -> HVariantF r2 f a
  -> c
onF p f g r =
  case coerceY r of
    HVariantFRep v | v.type == reflectSymbol p -> f v.value
    _ -> g (coerceR r)
  where
  coerceY ∷ HVariantF r2 f a -> HVariantFRep h f a
  coerceY = unsafeCoerce

  coerceR ∷ HVariantF r2 f a -> HVariantF r1 f a
  coerceR = unsafeCoerce

onMatchF
  ∷ forall rl r r1 r2 r3 a b c
  . RL.RowToList r rl
  => HVariantFMatchCases rl r1 a b
  => R.Union r1 r2 r3
  => Record r
  -> (HVariantF r2 a b -> c)
  -> HVariantF r3 a b
  -> c
onMatchF r k v =
  case coerceV v of
    HVariantFRep v' | unsafeHas v'.type r -> unsafeGet v'.type r v'.value
    _ → k (coerceR v)

  where
  coerceV ∷ forall h. HVariantF r3 a b -> HVariantFRep h a b
  coerceV = unsafeCoerce

  coerceR ∷ HVariantF r3 a b -> HVariantF r2 a b
  coerceR = unsafeCoerce

caseF_ ∷ forall a b c. HVariantF () a b -> c
caseF_ r = unsafeCrashWith case unsafeCoerce r of
  HVariantFRep v -> "Data.HFunctor.Variant: pattern match failure [" <> v.type <> "]"

matchF
  ∷ forall rl r r1 r2 a b c
  . RL.RowToList r rl
  => HVariantFMatchCases rl r1 a b
  => R.Union r1 () r2
  => Record r
  -> HVariantF r2 a b
  -> c
matchF r = caseF_ # onMatchF r

defaultF :: forall a b c r. a -> HVariantF r b c -> a
defaultF a _ = a

expandF :: forall lt mix gt a b. R.Union lt mix gt => HVariantF lt a b -> HVariantF gt a b
expandF = unsafeCoerce      

------------------------------------------------------------------------

newtype HMu (f :: (Type -> Type) -> (Type -> Type)) (a :: Type) = HMu (f (HMu f) a)

derive instance newtypeHMu :: Newtype (HMu f a) _

instance hrecursiveMu :: HFunctor f => HRecursive (HMu f) f where
  hproject = unwrap

instance eqHMu :: (Eq a, Eq1 (f (HMu f))) => Eq (HMu f a) where
  eq (HMu x) (HMu y) = eq1 x y

instance ordHMu :: (Ord a, Ord1 (f (HMu f))) => Ord (HMu f a) where
  compare (HMu x) (HMu y) = compare1 x y

instance semigroupHMu :: Alt (f (HMu f)) => Semigroup (HMu f a) where
  append (HMu x) (HMu y) = HMu (x <|> y)

instance monoidHMu :: Plus (f (HMu f)) => Monoid (HMu f a) where
  mempty = HMu empty

class HFunctor (h :: (Type -> Type) -> Type -> Type) where
  hmap :: forall f g. (f ~> g) -> h f ~> h g

type HAlgebra h f = h f ~> f

class HFunctor f <= HRecursive t f | t -> f where
  hproject ∷ t ~> f t

class HFunctor f <= Corecursive t f | t -> f where
  hembed ∷ f t ~> t

hcata :: forall h f t. HFunctor h => HRecursive t h => HAlgebra h f -> t ~> f
hcata algebra t = algebra (hmap (hcata algebra) (hproject t))

type HEADT t = HMu (HVariantF t)

injHEADT 
  ∷ forall h s a b
  . R.Cons s (HProxy h) a b 
  => IsSymbol s 
  => HFunctor h 
  => SProxy s 
  -> HAlgebra h (HEADT b)
injHEADT label = wrap <<< injF label

----------------------------------------------------------------

data Value a
  = VInt Int (a ~ Int)
  | VBool Boolean (a ~ Boolean)

instance showValue :: Show a => Show (Value a) where
  show = case _ of
    VInt a p -> "VInt " <> show (coerceSymm p a)
    VBool a p -> "VBool " <> show (coerceSymm p a)

data AddF h p = AddF (h Int) (h Int) (p ~ Int)

instance hfunctorAddF :: HFunctor AddF where
  hmap g (AddF x y p) = AddF (g x) (g y) p

data ValF (h :: Type -> Type) p = ValF Int (p ~ Int)

instance hfunctorValF :: HFunctor ValF where
  hmap _ (ValF x p) = ValF x p

data MulF h p = MulF (h Int) (h Int) (p ~ Int)

instance hfunctorMulF :: HFunctor MulF where
  hmap g (MulF x y p) = MulF (g x) (g y) p

data EqualF h p = EqualF (h Int) (h Int) (p ~ Boolean)

instance hfunctorEqualF :: HFunctor EqualF where
  hmap g (EqualF x y p) = EqualF (g x) (g y) p

data NotF h p = NotF (h Boolean) (p ~ Boolean)

instance hfunctorNotF :: HFunctor NotF where
  hmap g (NotF x p) = NotF (g x) p

data BoolF (h :: Type -> Type) p = BoolF Boolean (p ~ Boolean)

instance hfuctorBoolF :: HFunctor BoolF where
  hmap _ (BoolF x p) = BoolF x p

data LessThanF h p = LessThanF (h Int) (h Int) (p ~ Boolean)

instance hfuctorLessThanF :: HFunctor LessThanF where
  hmap g (LessThanF x y p) = LessThanF (g x) (g y) p

data IfF h p = IfF (h Boolean) (h p) (h p) (Either (p ~ Int) (p ~ Boolean))

instance hfuctorIfF :: HFunctor IfF where
  hmap g (IfF c x y p) = IfF (g c) (g x) (g y) p

evalAlgebra :: forall r a. (HVariantF r Identity a -> Identity a) -> HVariantF (Val + Add + r) Identity a -> Identity a 
evalAlgebra = onMatchF
  { valF: \(ValF x p) -> Identity $ coerceSymm p x
  , addF: \(AddF (Identity x) (Identity y) p) -> Identity $ coerceSymm p $ x + y
  }

_valF = SProxy :: SProxy "valF"
_addF = SProxy :: SProxy "addF"
_mulF = SProxy :: SProxy "mulF"
_notF = SProxy :: SProxy "notF"
_equalF = SProxy :: SProxy "equalF"
_boolF = SProxy :: SProxy "boolF"
_ifF = SProxy :: SProxy "ifF"
_lessThanF = SProxy :: SProxy "lessThanF"

type Val r = (valF ∷ HProxy ValF | r)
type Add r = (addF ∷ HProxy AddF | r)
type Mul r = (mulF ∷ HProxy MulF | r)
type Not r = (notF ∷ HProxy NotF | r)
type Equal r = (equalF ∷ HProxy EqualF | r)
type Bool r = (boolF :: HProxy BoolF | r)
type LessThan r = (lessThanF :: HProxy LessThanF | r)
type If r = (ifF :: HProxy IfF | r)

valF :: forall r. Int -> HEADT (Val + r) Int
valF x = injHEADT _valF (ValF x identity)

addF :: forall r. HEADT (Add + r) Int -> HEADT (Add + r) Int -> HEADT (Add + r) Int
addF x y = injHEADT _addF (AddF x y identity)

mulF :: forall r. HEADT (Mul + r) Int -> HEADT (Mul + r) Int -> HEADT (Mul + r) Int
mulF x y = injHEADT _mulF (MulF x y identity)

notF :: forall r. HEADT (Not + r) Boolean -> HEADT (Not + r) Boolean
notF x = injHEADT _notF (NotF x identity)

equalF :: forall r. HEADT (Equal + r) Int -> HEADT (Equal + r) Int -> HEADT (Equal + r) Boolean
equalF x y = injHEADT _equalF (EqualF x y identity)

boolF :: forall r. Boolean -> HEADT (Bool + r) Boolean
boolF x = injHEADT _boolF (BoolF x identity)

ifF :: forall r a. HEADT (If + r) Boolean -> HEADT (If + r) a -> HEADT (If + r) a -> Either (a ~ Int) (a ~ Boolean) -> HEADT (If + r) a
ifF c x y p = injHEADT _ifF (IfF c x y p)

evalAlgebra2 :: forall r a. (HVariantF r Identity a -> Identity a) -> HVariantF (Val + Add + Mul + Not + Equal + r) Identity a -> Identity a 
evalAlgebra2 = evalAlgebra 
  >>> onMatchF 
    { mulF: \(MulF (Identity x) (Identity y) p) -> Identity $ coerceSymm p $ x * y
    , notF: \(NotF (Identity x) p) -> Identity $ coerceSymm p $ not $ x
    , equalF: \(EqualF (Identity x) (Identity y) p) -> Identity $ coerceSymm p $ x == y
    }

value :: HEADT (Not + Equal + Mul + Add + Val + ()) Boolean
value = notF (equalF (mulF (valF 10) (valF 1)) (addF (valF 0) (valF 1)))

value2 :: HEADT (If + Bool + Add + Val + ()) Int
value2 = ifF (boolF false) (valF 1) (addF (valF 42) (valF 45)) (Left identity)

evalAlgebra3 :: forall r a. (HVariantF r Identity a -> Identity a) -> HVariantF (Val + Add + Bool + If + r) Identity a -> Identity a 
evalAlgebra3 = evalAlgebra 
  >>> onMatchF 
    { boolF: \(BoolF x p) -> Identity $ coerceSymm p x
    , ifF: \(IfF (Identity c) (Identity x) (Identity y) p) -> Identity $ if c then x else y
    }

evalValueAlgebra :: forall a. Partial => HVariantF (Val + Bool + Mul + Add + Equal + Not + If + LessThan + ()) Value a -> Value a
evalValueAlgebra = matchF
  { valF: \(ValF x p) -> VInt x p
  , boolF: \(BoolF x p) -> VBool x p
  , mulF: \(MulF (VInt x _) (VInt y _) p) -> VInt (x * y) p
  , addF: \(AddF (VInt x _) (VInt y _) p) -> VInt (x + y) p
  , equalF: \(EqualF (VInt x _) (VInt y _) p) -> VBool (x == y) p
  , notF: \(NotF (VBool x _) p) -> VBool (not x) p
  , lessThanF: \(LessThanF (VInt x _) (VInt y _) p) -> VBool (x < y) p
  , ifF: \(IfF (VBool c _) x y p) -> if c then x else y
  }