HFree + QuantifiedConstraints

gistfile1.hs

-- Response to
--   https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
--   https://twitter.com/sjoerd_visscher/status/975375241932427265

{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}

import Data.Coerce

type f ~> g = forall x. f x -> g x

class BaseSem sem where
  val :: a -> sem a
  add :: sem Int -> sem Int -> sem Int

class BaseSem sem => BoolSem sem where
  iff :: sem Bool -> sem a -> sem a -> sem a
  gte :: sem Int -> sem Int -> sem Bool

expr :: BoolSem sem => sem Int
expr = iff (gte (val 10) (val 20)) (val 100) (val 200)

newtype E a = E { eval :: a } deriving (Show)
instance BaseSem E where
  val = E
  add x y = E $ eval x + eval y

instance BoolSem E where
  iff b t e = E $ if eval b then eval t else eval e
  gte x y = E $ eval x >= eval y

data HFree cls f a where
  HFree :: (forall xx. cls xx => (f ~> xx) -> xx a) -> HFree cls f a

class    (forall xx. f xx => g xx) => f ~=> g
instance (forall xx. f xx => g xx) => f ~=> g

instance base ~=> BaseSem => BaseSem (HFree base f) where
  val :: a -> HFree base f a
  val a = HFree (\_ -> val a)

  add :: HFree base f Int -> HFree base f Int -> HFree base f Int
  HFree xsWith `add` HFree ysWith = HFree $ \k -> 
    xsWith k `add` ysWith k

instance bool ~=> BoolSem => BoolSem (HFree bool f) where
  iff :: HFree bool f Bool -> HFree bool f a -> HFree bool f a -> HFree bool f a
  iff (HFree condWith) (HFree trueWith) (HFree falseWith) = HFree $ \k -> 
    iff (condWith k) (trueWith k) (falseWith k)

  gte :: HFree bool f Int -> HFree bool f Int -> HFree bool f Bool
  HFree xsWith `gte` HFree ysWith = HFree $ \k -> 
    xsWith k `gte` ysWith k

data Vars a where
  Int  :: String -> Vars Int
  Bool :: String -> Vars Bool

test :: HFree BoolSem Vars Int
test = add expr (unit (Int "x"))

unit :: f ~> HFree cls f
unit xs = HFree ($ xs)

rightAdjunct :: c g => (f ~> g) -> (HFree c f ~> g)
rightAdjunct k (HFree xsWith) = xsWith k

main :: IO ()
main = print $ rightAdjunct lookupVar test where
  lookupVar :: Vars ~> E
  lookupVar (Int "x") = E 10
  lookupVar _ = error "unknown variable"

Same example with a universe (deeply indexed by) data Ty = I | B

{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs, DataKinds, StandaloneDeriving, TypeFamilyDependencies #-}

import Data.Kind
import Data.Coerce

type f ~> g = forall x. f x -> g x

data Ty = I | B

type family
  Interp (ty :: Ty) = (res :: Type) | res -> ty where
  Interp 'I = Int
  Interp 'B = Bool

class BaseSem sem where
  val :: Interp a -> sem a
  add :: sem I -> sem I -> sem I

class BaseSem sem => BoolSem sem where
  iff :: sem B -> sem a -> sem a -> sem a
  gte :: sem I -> sem I -> sem B

expr :: BoolSem sem => sem I
expr = iff (gte (val 10) (val 20)) (val 100) (val 200)

newtype E a = E { eval :: Interp a } 
deriving instance Show (Interp a) => Show (E a)

instance BaseSem E where
  val = E
  add x y = E $ eval x + eval y

instance BoolSem E where
  iff b t e = E $ if eval b then eval t else eval e
  gte x y = E $ eval x >= eval y

data HFree :: ((k -> Type) -> Constraint) -> (k -> Type) -> (k -> Type) where
  HFree :: (forall xx. cls xx => (f ~> xx) -> xx a) -> HFree cls f a

class    (forall xx. f xx => g xx) => f ~=> g
instance (forall xx. f xx => g xx) => f ~=> g

instance base ~=> BaseSem => BaseSem (HFree base f) where
  val :: Interp a -> HFree base f a
  val a = HFree $ \_ -> 
    val a

  add :: HFree base f I -> HFree base f I -> HFree base f I
  HFree xsWith `add` HFree ysWith = HFree $ \k -> 
    xsWith k `add` ysWith k

instance bool ~=> BoolSem => BoolSem (HFree bool f) where
  iff :: HFree bool f B -> HFree bool f a -> HFree bool f a -> HFree bool f a
  iff (HFree condWith) (HFree trueWith) (HFree falseWith) = HFree $ \k -> 
    iff (condWith k) (trueWith k) (falseWith k)

  gte :: HFree bool f I -> HFree bool f I -> HFree bool f B
  HFree xsWith `gte` HFree ysWith = HFree $ \k -> 
    xsWith k `gte` ysWith k

data Vars a where
  Int  :: String -> Vars I
  Bool :: String -> Vars B

test :: HFree BoolSem Vars I
test = add expr (unit (Int "x"))

unit :: f ~> HFree cls f
unit xs = HFree ($ xs)

rightAdjunct :: c g => (f ~> g) -> (HFree c f ~> g)
rightAdjunct k (HFree xsWith) = xsWith k

main :: IO ()
main = print $ rightAdjunct lookupVar test where
  lookupVar :: Vars ~> E
  lookupVar (Int "x") = E 10
  lookupVar _ = error "unknown variable"