Skip to content

Instantly share code, notes, and snippets.

@rrnewton

rrnewton/bad_output.hs

Last active August 29, 2015 14:24
Show Gist options
  • Save rrnewton/12f82aa42d4f77775a55 to your computer and use it in GitHub Desktop.
Save rrnewton/12f82aa42d4f77775a55 to your computer and use it in GitHub Desktop.
Download ZIP
Bad output with unfinished bits
Raw
bad_output.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Ghostbuster where
import Prelude hiding (Int, Maybe(..), Bool(..))
data TypeDict a where
data TyEquality a b where
Refl :: TyEquality a a
data Typ a where
Int :: Typ Int
Arr :: Typ a -> Typ b -> Typ (a -> b)
data Var e a where
Zro :: Var (Tup2 e a) a
Suc :: Var e a -> Var (Tup2 e b) a
data Exp e a where
Con :: Int -> Exp e Int
Add :: Exp e Int -> Exp e Int -> Exp e Int
Mul :: Exp e Int -> Exp e Int -> Exp e Int
Var :: Var e a -> Exp e a
Abs :: Typ a -> Exp (Tup2 e a) b -> Exp e (a -> b)
App :: Exp e (a -> b) -> Exp e a -> Exp e b
data Typ' where
Int' :: Typ'
Arr' :: Typ' -> Typ' -> Typ'
deriving Show
data SealedTyp where
SealedTyp :: TypeDict a -> Typ a -> SealedTyp
data Var' where
Zro' :: Var'
Suc' :: Var' -> Var'
deriving Show
data SealedVar e where
SealedVar :: TypeDict a -> Var e a -> SealedVar e
data Exp' where
Con' :: Int -> Exp'
Add' :: Exp' -> Exp' -> Exp'
Mul' :: Exp' -> Exp' -> Exp'
Var' :: Var' -> Exp'
Abs' :: Typ' -> Exp' -> Exp'
App' :: Exp' -> Exp' -> Exp'
deriving Show
data SealedExp e where
SealedExp :: TypeDict a -> Exp e a -> SealedExp e
data ArrowTy a b where
data Int where
One :: Int
Two :: Int
Three :: Int
deriving Show
data Maybe a where
Just :: a -> Maybe a
Nothing :: Maybe a
deriving Show
data Bool where
True :: Bool
False :: Bool
deriving Show
data Tup2 a b where
Tup2 :: a -> b -> Tup2 a b
deriving Show
downTyp :: forall a . TypeDict a -> Typ a -> Typ'
downTyp a_dict orig
= case orig of
Int -> Int'
Arr a b -> Arr' (downTyp UNFINISHED:VarTy (Var "a") a)
(downTyp UNFINISHED:VarTy (Var "b") b)
downVar :: forall e a . TypeDict e -> TypeDict a -> Var e a -> Var'
downVar e_dict a_dict orig
= case orig of
Zro -> Zro'
Suc a -> Suc'
(downVar UNFINISHED:VarTy (Var "e") UNFINISHED:VarTy (Var "a") a)
downExp :: forall e a . TypeDict e -> TypeDict a -> Exp e a -> Exp'
downExp e_dict a_dict orig
= case orig of
Con a -> Con' (downInt a)
Add a b -> Add'
(downExp UNFINISHED:VarTy (Var "e") UNFINISHED:ConTy (Var "Int") []
a)
(downExp UNFINISHED:VarTy (Var "e") UNFINISHED:ConTy (Var "Int") []
b)
Mul a b -> Mul'
(downExp UNFINISHED:VarTy (Var "e") UNFINISHED:ConTy (Var "Int") []
a)
(downExp UNFINISHED:VarTy (Var "e") UNFINISHED:ConTy (Var "Int") []
b)
Var a -> Var'
(downVar UNFINISHED:VarTy (Var "e") UNFINISHED:VarTy (Var "a") a)
Abs a b -> Abs' (downTyp UNFINISHED:VarTy (Var "a") a)
(downExp
UNFINISHED:ConTy (Var "Tup2") [VarTy (Var "e"),VarTy (Var "a")]
UNFINISHED:VarTy (Var "b")
b)
App a b -> App'
(downExp UNFINISHED:VarTy (Var "e")
UNFINISHED:ArrowTy (VarTy (Var "a")) (VarTy (Var "b"))
a)
(downExp UNFINISHED:VarTy (Var "e") UNFINISHED:VarTy (Var "a") b)
ghostbuster :: Int
ghostbuster = Three
main :: IO ()
main = print ghostbuster
Raw
getting_closer.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Ghostbuster where
import Prelude hiding (Int, Maybe(..), Bool(..))
data TypeDict a where
ArrowTyDict :: TypeDict a -> TypeDict b -> TypeDict (ArrowTy a b)
IntDict :: TypeDict Int
Tup2Dict :: TypeDict a -> TypeDict b -> TypeDict (Tup2 a b)
data TyEquality a b where
Refl :: TyEquality a a
data Typ a where
Int :: Typ Int
Arr :: Typ a -> Typ b -> Typ (a -> b)
data Var e a where
Zro :: Var (Tup2 e a) a
Suc :: Var e a -> Var (Tup2 e b) a
data Exp env ans where
Con :: Int -> Exp e1 Int
Add :: Exp e2 Int -> Exp e2 Int -> Exp e2 Int
Mul :: Exp e3 Int -> Exp e3 Int -> Exp e3 Int
Var :: Var e4 u -> Exp e4 u
Abs :: Typ r -> Exp (Tup2 e5 r) s -> Exp e5 (r -> s)
App :: Exp e6 (x -> y) -> Exp e6 x -> Exp e6 y
data Typ' where
Int' :: Typ'
Arr' :: Typ' -> Typ' -> Typ'
deriving Show
data SealedTyp where
SealedTyp :: TypeDict a -> Typ a -> SealedTyp
data Var' where
Zro' :: Var'
Suc' :: Var' -> Var'
deriving Show
data SealedVar e where
SealedVar :: TypeDict a -> Var e a -> SealedVar e
data Exp' where
Con' :: Int -> Exp'
Add' :: Exp' -> Exp' -> Exp'
Mul' :: Exp' -> Exp' -> Exp'
Var' :: Var' -> Exp'
Abs' :: Typ' -> Exp' -> Exp'
App' :: Exp' -> Exp' -> Exp'
deriving Show
data SealedExp env where
SealedExp :: TypeDict ans -> Exp env ans -> SealedExp env
data ArrowTy a b where
data Int where
One :: Int
Two :: Int
Three :: Int
deriving Show
data Maybe a where
Just :: a -> Maybe a
Nothing :: Maybe a
deriving Show
data Bool where
True :: Bool
False :: Bool
deriving Show
data Tup2 a b where
Tup2 :: a -> b -> Tup2 a b
deriving Show
checkTEQ :: TypeDict t -> TypeDict u -> Maybe (TyEquality t u)
checkTEQ x y
= case x of
ArrowTyDict a1 b1 -> case y of
ArrowTyDict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> Nothing
IntDict -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Just Refl
Tup2Dict a2 b2 -> Nothing
Tup2Dict a1 b1 -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
downTyp :: forall a . TypeDict a -> Typ a -> Typ'
downTyp a_dict orig
= case orig of
Int -> Int'
Arr a b -> Arr' (downTyp a_dict a) (downTyp b_dict b)
downVar :: forall e a . TypeDict e -> TypeDict a -> Var e a -> Var'
downVar e_dict a_dict orig
= case orig of
Zro -> Zro'
Suc a -> Suc' (downVar e_dict a_dict a)
downExp ::
forall env ans .
TypeDict env -> TypeDict ans -> Exp env ans -> Exp'
downExp env_dict ans_dict orig
= case orig of
Con a -> Con' a
Add a b -> Add' (downExp e2_dict IntDict a)
(downExp e2_dict IntDict b)
Mul a b -> Mul' (downExp e3_dict IntDict a)
(downExp e3_dict IntDict b)
Var a -> Var' (downVar e4_dict u_dict a)
Abs a b -> Abs' (downTyp r_dict a)
(downExp (Tup2Dict e5_dict r_dict) s_dict b)
App a b -> App' (downExp e6_dict (ArrowTyDict x_dict y_dict) a)
(downExp e6_dict x_dict b)
ghostbuster :: Int
ghostbuster = Three
main :: IO ()
main = print ghostbuster
Raw
manually_fixed.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Ghostbuster where
import Prelude hiding (Int, Maybe(..), Bool(..))
data TypeDict a where
ArrowTyDict :: TypeDict a -> TypeDict b -> TypeDict (a -> b)
IntDict :: TypeDict Int
Tup2Dict :: TypeDict a -> TypeDict b -> TypeDict (Tup2 a b)
data TyEquality a b where
Refl :: TyEquality a a
data Typ a where
Int :: Typ Int
Arr :: Typ v -> Typ w -> Typ (v -> w)
data Var env ans where
Zro :: Var (Tup2 e1 a) a
Suc :: Var e2 x -> Var (Tup2 e2 y) x
data Exp env ans where
Con :: Int -> Exp e1 Int
Add :: Exp e2 Int -> Exp e2 Int -> Exp e2 Int
Mul :: Exp e3 Int -> Exp e3 Int -> Exp e3 Int
Var :: Var e4 u -> Exp e4 u
Abs :: Typ r -> Exp (Tup2 e5 r) s -> Exp e5 (r -> s)
App :: Exp e6 (x -> y) -> Exp e6 x -> Exp e6 y
data Typ' where
Int' :: Typ'
Arr' :: Typ' -> Typ' -> Typ'
deriving Show
data SealedTyp where
SealedTyp :: TypeDict a -> Typ a -> SealedTyp
data Var' where
Zro' :: Var'
Suc' :: Var' -> Var'
deriving Show
data SealedVar env where
SealedVar :: TypeDict ans -> Var env ans -> SealedVar env
data Exp' where
Con' :: Int -> Exp'
Add' :: Exp' -> Exp' -> Exp'
Mul' :: Exp' -> Exp' -> Exp'
Var' :: Var' -> Exp'
Abs' :: Typ' -> Exp' -> Exp'
App' :: Exp' -> Exp' -> Exp'
deriving Show
data SealedExp env where
SealedExp :: TypeDict ans -> Exp env ans -> SealedExp env
data ArrowTy a b where
data Int where
One :: Int
Two :: Int
Three :: Int
deriving Show
data Maybe a where
Just :: a -> Maybe a
Nothing :: Maybe a
deriving Show
data Bool where
True :: Bool
False :: Bool
deriving Show
data Tup2 a b where
Tup2 :: a -> b -> Tup2 a b
deriving Show
checkTEQ :: TypeDict t -> TypeDict u -> Maybe (TyEquality t u)
checkTEQ x y
= case x of
ArrowTyDict a1 b1 -> case y of
ArrowTyDict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> Nothing
IntDict -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Just Refl
Tup2Dict a2 b2 -> Nothing
Tup2Dict a1 b1 -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
downTyp :: forall a . TypeDict a -> Typ a -> Typ'
downTyp a_dict orig
= case orig of
Int -> Int'
Arr a b ->
case a_dict of
ArrowTyDict vd wd -> Arr' (downTyp vd a) (downTyp wd b)
downVar ::
forall env ans .
TypeDict env -> TypeDict ans -> Var env ans -> Var'
downVar env_dict ans_dict orig
= case orig of
Zro -> Zro'
Suc a ->
case env_dict of
Tup2Dict ad _ -> Suc' (downVar ad ans_dict a)
downExp ::
forall env ans .
TypeDict env -> TypeDict ans -> Exp env ans -> Exp'
downExp env_dict ans_dict orig
= case orig of
Con a -> Con' a
Add a b -> Add' (downExp env_dict IntDict a)
(downExp env_dict IntDict b)
Mul a b -> Mul' (downExp env_dict IntDict a)
(downExp env_dict IntDict b)
Var a -> Var' (downVar env_dict ans_dict a)
Abs a b -> case ans_dict of
ArrowTyDict r_dict s_dict ->
Abs' (downTyp r_dict a)
(downExp (Tup2Dict env_dict r_dict) s_dict b)
App a b -> let arg_dict = error "unused"
in App' (downExp env_dict (ArrowTyDict arg_dict ans_dict) a)
(downExp env_dict arg_dict b)
ghostbuster :: Exp'
ghostbuster = downExp IntDict IntDict (Add (Con Three) (Con Two))
main :: IO ()
main = print ghostbuster
Raw
manually_fixed2.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Ghostbuster where
import Prelude hiding (Int, Maybe(..), Bool(..))
data TypeDict a where
ArrowTyDict :: TypeDict a -> TypeDict b -> TypeDict (a -> b)
IntDict :: TypeDict Int
Tup2Dict :: TypeDict a -> TypeDict b -> TypeDict (Tup2 a b)
UnitDict :: TypeDict ()
data TyEquality a b where
Refl :: TyEquality a a
data Typ a where
Int :: Typ Int
Arr :: Typ v -> Typ w -> Typ (v -> w)
data Var env ans where
Zro :: Var (Tup2 e1 a) a
Suc :: Var e2 x -> Var (Tup2 e2 y) x
data Exp env ans where
Con :: Int -> Exp e1 Int
Add :: Exp e2 Int -> Exp e2 Int -> Exp e2 Int
Mul :: Exp e3 Int -> Exp e3 Int -> Exp e3 Int
Var :: Var e4 u -> Exp e4 u
Abs :: Typ r -> Exp (Tup2 e5 r) s -> Exp e5 (r -> s)
App :: TypeDict x -> Exp e6 (x -> y) -> Exp e6 x -> Exp e6 y
data Typ' where
Int' :: Typ'
Arr' :: Typ' -> Typ' -> Typ'
deriving Show
data SealedTyp where
SealedTyp :: TypeDict a -> Typ a -> SealedTyp
data Var' where
Zro' :: Var'
Suc' :: Var' -> Var'
deriving Show
data SealedVar env where
SealedVar :: TypeDict ans -> Var env ans -> SealedVar env
data Exp' where
Con' :: Int -> Exp'
Add' :: Exp' -> Exp' -> Exp'
Mul' :: Exp' -> Exp' -> Exp'
Var' :: Var' -> Exp'
Abs' :: Typ' -> Exp' -> Exp'
App' :: TypeDict arg -> Exp' -> Exp' -> Exp'
-- deriving Show
data SealedExp env where
SealedExp :: TypeDict ans -> Exp env ans -> SealedExp env
data ArrowTy a b where
data Int where
One :: Int
Two :: Int
Three :: Int
deriving Show
data Maybe a where
Just :: a -> Maybe a
Nothing :: Maybe a
deriving Show
data Bool where
True :: Bool
False :: Bool
deriving Show
data Tup2 a b where
Tup2 :: a -> b -> Tup2 a b
deriving Show
checkTEQ :: TypeDict t -> TypeDict u -> Maybe (TyEquality t u)
checkTEQ x y
= case x of
ArrowTyDict a1 b1 -> case y of
ArrowTyDict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> Nothing
IntDict -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Just Refl
Tup2Dict a2 b2 -> Nothing
Tup2Dict a1 b1 -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Nothing
Tup2Dict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
downTyp :: forall a . TypeDict a -> Typ a -> Typ'
downTyp a_dict orig
= case orig of
Int -> Int'
Arr a b ->
case a_dict of
ArrowTyDict vd wd -> Arr' (downTyp vd a) (downTyp wd b)
downVar ::
forall env ans .
TypeDict env -> TypeDict ans -> Var env ans -> Var'
downVar env_dict ans_dict orig
= case orig of
Zro -> Zro'
Suc a ->
case env_dict of
Tup2Dict ad _ -> Suc' (downVar ad ans_dict a)
downExp ::
forall env ans .
TypeDict env -> TypeDict ans -> Exp env ans -> Exp'
downExp env_dict ans_dict orig
= case orig of
Con a -> Con' a
Add a b -> Add' (downExp env_dict IntDict a)
(downExp env_dict IntDict b)
Mul a b -> Mul' (downExp env_dict IntDict a)
(downExp env_dict IntDict b)
Var a -> Var' (downVar env_dict ans_dict a)
Abs a b -> case ans_dict of
ArrowTyDict r_dict s_dict ->
Abs' (downTyp r_dict a)
(downExp (Tup2Dict env_dict r_dict) s_dict b)
App arg_dict a b -> App' arg_dict
(downExp env_dict (ArrowTyDict arg_dict ans_dict) a)
(downExp env_dict arg_dict b)
ghostbuster :: Exp'
ghostbuster =
downExp emptyEnv IntDict $
(App (IntDict) (Abs Int (Var Zro)) (Con Two))
emptyEnv :: TypeDict ()
emptyEnv = UnitDict
-- emptyEnv = (error "empty env dict") -- This works too
-- emptyEnv = IntDict -- This works too.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment