{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data Hask :: * -> * where
  App :: Hask (a -> b) -> Hask a -> Hask b
  Abs :: (Hask a -> Hask b) -> Hask (a -> b)
  ValB :: Bool -> Hask Bool
  ValS :: String -> Hask String
  Loop :: Hask a -> Hask a
  Par :: Hask a -> Hask a -> Hask a

app :: Hask (a -> b) -> Hask a -> Hask b
app (Abs x) y = x y
app (App x y) z = App (app x y) z

step :: Hask a -> Hask a
step (App f a) = app f a
step (Abs f) = Abs f
step (ValB b) = ValB b
step (ValS s) = ValS s
step (Loop x) = Loop x
step (Par (ValB a) b) = ValB a
step (Par a (ValB b)) = ValB b
step (Par a b) = Par (step a) (step b)

sem :: Hask a -> Hask a
sem (App f a) = sem (app f a)
sem (Abs f) = (Abs f)
sem (ValB b) = (ValB b)
sem (ValS s) = (ValS s)
sem (Loop x) = sem (Loop x)
sem (Par a b) = sem (step (Par a b))

mshow (Loop _) = ValS "loop"
mshow (App _ _) = ValS "App"
mshow (ValB x) = ValS $ show x

instance Show (Hask a) where
  show (ValS s) = s
  show (ValB b) = show b

mor :: Hask Bool -> Hask Bool -> Hask Bool
mor x@(Loop _) z = App (App (Abs (\x -> (Abs (\y -> mor x y)))) x) z
mor (App x y) z = App (App (Abs (\x -> (Abs (\y -> mor x y)))) (app x y)) z
mor (ValB True) _ = ValB True
mor (ValB False) x = x

por :: Hask Bool -> Hask Bool -> Hask Bool
por x y = sem (Par (mor x y) (mor y x))

myid = Abs (\x -> x)
loop = Loop loop
b1 = ValB True
b2 = App myid b1
b3 = App myid b2

v1 = por loop b3
v2 = por b3 loop