CompLevels.hs

{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

module CompLevels where

import Control.Monad (forM_)

data Z
data S n

class LTE a b -- lower than or equal

instance LTE n n

instance LTE n m => LTE n (S m)

data Comp n a where
  Return :: a -> Comp n a
  Exec :: LTE m n => Comp m b -> (b -> Comp (S n) a) -> Comp (S n) a

execComp :: Comp n a -> a
execComp (Return v) = v
execComp (Exec c f) = execComp $ f $ execComp c

favouriteNumber :: Comp Z Int
favouriteNumber = Return 42

currentPlace :: Comp Z String
currentPlace = Return "World"

greet :: Comp n String -> Comp (S n) String
greet strComp = strComp `Exec` (\str -> Return ("Hello " ++ str ++ "!"))

mainComp :: Comp (S (S Z)) [String]
mainComp =
  favouriteNumber `Exec` \favNumber ->
  greet currentPlace `Exec` \greeting ->
  Return (replicate favNumber greeting)

main :: IO ()
main =
  let greetings = execComp mainComp
  in forM_ greetings putStrLn