Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Buggy Program
{-# 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 [])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment