Buggy Program

Buggy_Program.hs

{-# Language RankNTypes              #-}
{-# Language LambdaCase              #-}
{-# Language TypeOperators           #-}
{-# Language TypeApplications        #-}
{-# Language PolyKinds               #-}
{-# Language TypeFamilies            #-}
{-# Language FlexibleInstances       #-}
{-# Language GADTs                   #-}
{-# Language ConstraintKinds         #-}
{-# Language MultiParamTypeClasses   #-}
{-# Language FlexibleContexts        #-}
{-# Language QuantifiedConstraints   #-}
{-# Language UndecidableInstances    #-}
{-# Language UndecidableSuperClasses #-}
{-# Language InstanceSigs            #-}

import Prelude hiding ((>))

(>) = flip (.)

class    (f a, g a) => (Pair2___ f g) a
instance (f a, g a) => (Pair2___ f g) a

class    (f a b, g a b) => (Pair3___ f g) a b
instance (f a b, g a b) => (Pair3___ f g) a b

class    (a => b) => Implies a b
instance (a => b) => Implies a b

type f       ~> g = forall xx.                   f xx                   -> g xx
class    (forall xx. cls xx `Implies` cls' xx) => (cls ~=> cls')
instance (forall xx. cls xx `Implies` cls' xx) => (cls ~=> cls')

type family
  (&) :: k -> k -> k where
  (&) = Pair2___

newtype Yoneda f a = Yoneda (forall xx. (a -> xx) -> f xx)

----------------------------------------------------------------------
data Exp a where
  Con  :: String           -> Exp a
  Fun  :: Exp a -> [Exp a] -> Exp a
  Lift :: a                -> Exp a
instance Show a => Show (Exp a) where
 show = show' > unlines > init where

  show' :: Show a => Exp a -> [String]
  show' = \case
   Con str ->
    [str]
   Main.Fun f args ->
    show' f
    ++
    concatMap @[] (show' > map (' ':)) args
   Lift a -> [show a]
----------------------------------------------------------------------
infixr 5 ·
class List f where
  nil :: f a
  (·) :: a -> f a -> f a
instance List [] where
  nil :: [a]
  nil = []
  (·) :: a -> [a] -> [a]
  (·) = (:)
instance List Exp where
  nil :: Exp a
  nil = Con "nil"
  (·) :: a -> Exp a -> Exp a
  a · as = Main.Fun (Con "cons") [Lift a, as]
instance List f => List (Yoneda f) where
  nil :: Yoneda f a
  nil = Yoneda (\_ -> nil)
  (·) :: a -> Yoneda f a -> Yoneda f a
  a · Yoneda as = Yoneda (\f -> f a · as f)
----------------------------------------------------------------------
class Rev f where
  rev :: f ~> f
instance Rev f => Rev (Yoneda f) where
  rev :: Yoneda f ~> Yoneda f
  rev (Yoneda as) = Yoneda (\(f) -> rev (as f))
instance Rev [] where
  rev :: [] ~> []
  rev = reverse
instance Rev Exp where
  rev :: Exp a -> Exp a
  rev as = Main.Fun (Con "rev") [as]
instance cls ~=> Rev => Rev (Build cls) where
  rev :: Build cls ~> Build cls
  rev (Build as) = Build (rev as)
----------------------------------------------------------------------
as :: Exp a
as = Main.Fun (Con "f") [Main.Fun (Con "g") [Con "a", Con "b"], Main.Fun (Con "i") [Con "a", Con "b"]]

bs :: Rev f => List f => f Int
bs = rev $ 1·rev (2·rev (3·nil))

newtype Build cls a where
 Build
  :: (forall f. cls f => f a)
  -> Build cls a

bs' :: Build (Rev & List) Int
bs' = Build bs

uu = rev @(Build [])