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
|
{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables #-}
module ShouldCompile where
{-------- Examples from the paper ---------}
f :: (forall a. [a] -> a) -> (Int, Char)
f get = (get [1,2], get ['a', 'b', 'c'])
g :: Maybe (forall a. [a] -> a) -> (Int, Char)
g Nothing = (0, '0')
g (Just get) = (get [1,2], get ['a','b','c'])
sing x = [x]
id1 :: forall a. a -> a
id1 = id
{-
ids :: [forall a. a -> a]
ids = [id1,id1]
t1 :: [forall a. a -> a]
t1 = tail ids
t2 :: [forall a. a -> a]
t2 = sing id
t3 :: forall a. a -> a
t3 = head ids
-}
{--------------- Examples from QMLF paper -------------------}
qF :: (forall a. a -> a -> a) -> (Bool, Char)
qF choose = (choose True False, choose 'a' 'b')
qG :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall g. (g -> g) -> (g -> g))
qG choose id = choose id
qH :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall b. b -> b) -> (forall b. b -> b)
qH choose id = choose id
choose :: forall a. a -> a -> a
choose x y = x
{-
impred1 :: (Bool, Char)
impred1 = qF $ choose --- impredicative instantiation for $
impred2 :: (forall a. a -> a -> a) -> (Bool, Char)
impred2 = id qF
-}
{------ Examples for Garrique/Remy paper -------}
--- all of these currently work in GHC with higher-rank types
self1 :: (forall a. a -> a) -> (forall a. a -> a)
self1 f = f f
self2 :: (forall a. a -> a) -> b -> b
self2 f = f f
gr1 = self1 id
gr2 = self2 id
gr3 = (\(u :: (forall a. a -> a) -> (forall a. a -> a)) -> u id) self1
{------------ Church numerals ----------}
type Church = forall a. a -> (a -> a) -> a
z :: Church
z = \z -> \f -> z
s :: Church -> Church
s = \n -> \z -> \f -> f (n z f)
fold :: Church -> a -> (a -> a) -> a
fold n f z = n f z
{-
mul :: Church -> Church -> Church
mul m n = \f -> \a -> m (n f) a
exp :: Church -> Church -> Church
exp m n = n (mul m) (s z)
idC :: Church -> Church
idC x = fold x s z
inc :: Church -> Church
inc x = fold x s (s z)
-}
{------- fix for higher rank types ---------}
data Tree a = Branch a (Tree (a,a)) | Leaf
type MapTree = forall a b. (a -> b) -> Tree a -> Tree b
cross f (a,b) = (f a,f b)
-- I think this should work in GHC now, but it doesn't
-- fix specialized to higher-rank type
fixMT :: (MapTree -> MapTree) -> MapTree
fixMT f = f (fixMT f)
mapTree' = fixMT (\ (mapTree :: MapTree) -> \f tree -> case tree of
Branch a t -> Branch (f a) (mapTree (cross f) t)
Leaf -> Leaf)
-- polymorphic fix
fix :: (a -> a) -> a
fix f = f (fix f)
-- mapTree'' :: MapTree
mapTree'' = (fix :: (MapTree -> MapTree) -> MapTree)
(\ mapTree -> \f tree -> case tree of
Branch a t -> Branch (f a) (mapTree (cross f) t)
Leaf -> Leaf)
|
