hfree example.hs

{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, RankNTypes, GADTs, TypeOperators, UndecidableInstances, ConstraintKinds, DataKinds , ScopedTypeVariables #-}

import Data.Constraint
import Data.Constraint.Class1
import Data.Functor.HFree

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 v = E v
  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

instance HasSuperClasses BaseSem
instance HasSuperClasses BoolSem where
  type SuperClasses BoolSem = BoolSem ': SuperClasses BaseSem
  superClasses = Sub Dict
  containsSelf = Sub Dict

instance SuperClass1 BaseSem c => BaseSem (HFree c f) where
  val v = HFree $ \_ -> h scls1 v
    where
      h :: c g => (c g :- BaseSem g) -> a -> g a
      h (Sub Dict) = val
  add (HFree x) (HFree y) = HFree $ \k -> h scls1 (x k) (y k)
    where
      h :: c g => (c g :- BaseSem g) -> g Int -> g Int -> g Int
      h (Sub Dict) = add
      
instance SuperClass1 BoolSem c => BoolSem (HFree c f) where
  iff (HFree b) (HFree t) (HFree e) = HFree $ \k -> h scls1 (b k) (t k) (e k)
    where
      h :: c g => (c g :- BoolSem g) -> g Bool -> g a -> g a -> g a
      h (Sub Dict) = iff
  gte (HFree x) (HFree y) = HFree $ \k -> h scls1 (x k) (y k)
    where
      h :: c g => (c g :- BoolSem g) -> g Int -> g Int -> g Bool
      h (Sub Dict) = gte

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

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

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

Rewritten with -XQuantifiedConstraints: https://gist.github.com/Icelandjack/3a98d3979879fd9415bbde3761c51760