-
Notifications
You must be signed in to change notification settings - Fork 0
/
taglessfinal2.hs
143 lines (122 loc) · 4.29 KB
/
taglessfinal2.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
{-# OPTIONS_GHC -W #-}
-- After reading "Finally Tagless, Partially Evaluated"
module TaglessFinal2 where
import qualified Data.Function as F (fix)
-- There are some essence of tagless final that wasn't captured in our previous
-- file (i.e., taglessfinal.hs)
--
-- Take the algebra below as an example, following our previous recipe
class Bad t where
bool_bad :: Bool -> t
lam_bad :: (t -> t) -> t
app_bad :: t -> t -> t
-- This still type check, so the type still fails to capture the well-typedness
-- of our language
test :: (Bad f) => f
test = app_bad (bool_bad True) (bool_bad False)
-- This is because we use a type param `t` to encapsulate the entire representation
-- of our language, thus essentially "uni-typed" our object language.
class Good repr where
bool_good :: Bool -> repr Bool
lam_good :: (repr a -> repr b) -> repr (a -> b)
app_good :: repr (a -> b) -> repr a -> repr b
-- And now the term below doesn't type check!
--
-- test_should_fail :: (Good f) => f a
-- test_should_fail = app_good (bool_good True) (bool_good False)
-- Let's do the language in the paper!
-- The interface gives the syntax of the language,
-- and its instances give the semantics
class Algebra repr where
int :: Int -> repr Int
bool :: Bool -> repr Bool
lam :: (repr a -> repr b) -> repr (a -> b)
app :: repr (a -> b) -> repr a -> repr b
-- it seems also fine to define fix as:
-- fix :: repr (a -> a) -> repr a
-- just need to additionally use a `lam` when constructing terms
-- The current definition simplifies our instance definition (see below)
fix :: (repr a -> repr a) -> repr a
add :: repr Int -> repr Int -> repr Int
sub :: repr Int -> repr Int -> repr Int
mul :: repr Int -> repr Int -> repr Int
leq :: repr Int -> repr Int -> repr Bool
if_ :: repr Bool -> repr a -> repr a -> repr a
fibF' :: (Int -> Int) -> Int -> Int
fibF' =
\f ->
\n ->
if n == 0
then 0
else if n == 1
then 1
else f (n - 1) + f (n - 2)
fibF :: (Algebra repr) => repr (Int -> Int) -> repr (Int -> Int)
fibF =
\f -> lam (\n ->
if_ (leq n (int 0))
(int 0)
(if_ (leq n (int 1))
(int 1)
(add
(app f (sub n (int 1)))
(app f (sub n (int 2))))))
fib :: (Algebra repr) => repr (Int -> Int)
fib = fix fibF
-- this is kinda verbose, but...
newtype R a = R {unR :: a}
deriving (Show)
instance Algebra R where
int :: Int -> R Int
int = R
bool :: Bool -> R Bool
bool = R
lam :: (R a -> R b) -> R (a -> b)
lam f = R $ \a -> unR $ f (R a)
app :: R (a -> b) -> R a -> R b
app (R f) (R a) = R (f a)
fix :: (R a -> R a) -> R a
fix = F.fix
add :: R Int -> R Int -> R Int
add (R x) (R y) = R $ x + y
sub :: R Int -> R Int -> R Int
sub (R x) (R y) = R $ x - y
mul :: R Int -> R Int -> R Int
mul (R x) (R y) = R $ x * y
leq :: R Int -> R Int -> R Bool
leq (R x) (R y) = R $ x <= y
if_ :: R Bool -> R a -> R a -> R a
if_ (R b) (R t) (R e) = R $ if b then t else e
evalR :: R a -> a
evalR = unR
type Counter = Int
freshen :: Counter -> String
freshen c = "v" ++ show c
newtype S a = S {unS :: Counter -> String}
instance Algebra S where
int :: Int -> S Int
int n = S $ const (show n)
bool :: Bool -> S Bool
bool b = S $ const (show b)
lam :: (S a -> S b) -> S (a -> b)
lam f = S $ \c ->
let v = freshen c in
"(\\ " ++ v ++ " . " ++ unS (f (S $ const v)) (c + 1) ++ ")"
app :: S (a -> b) -> S a -> S b
app (S f) (S a) = S $ \c -> "(" ++ f c ++ " " ++ a c ++ ")"
fix :: (S a -> S a) -> S a
fix f = S $ \c ->
let v = freshen c in
"(fix " ++ v ++ " . " ++ unS (f (S $ const v)) (c + 1) ++ ")"
add :: S Int -> S Int -> S Int
add (S x) (S y) = S $ \c -> "(" ++ x c ++ " + " ++ y c ++ ")"
sub :: S Int -> S Int -> S Int
sub (S x) (S y) = S $ \c -> "(" ++ x c ++ " - " ++ y c ++ ")"
mul :: S Int -> S Int -> S Int
mul (S x) (S y) = S $ \c -> "(" ++ x c ++ " * " ++ y c ++ ")"
leq :: S Int -> S Int -> S Bool
leq (S x) (S y) = S $ \c -> "(" ++ x c ++ " <= " ++ y c ++ ")"
if_ :: S Bool -> S a -> S a -> S a
if_ (S b) (S x) (S y) = S $ \c -> "(if " ++ b c ++ " then " ++ x c ++ " else " ++ y c ++ ")"
evalS :: S a -> String
evalS s = unS s 0