Commit 048c91d1 authored by simonpj's avatar simonpj
Browse files

[project @ 2006-01-06 16:12:42 by simonpj]

Add tests for boxy types
parent 7d53bf6f
{-# OPTIONS_GHC -fglasgow-exts #-}
module Base1 where
-- basic examples of impredicative instantiation of variables
data MEither a b = MLeft a
| MRight b
| MEmpty
type Sid = forall a. a -> a
-- no need for impredicativity
test0 = MRight id
-- requires impredicativity
test1 :: Sid -> MEither Sid b
test1 fid = MLeft fid
test2 :: MEither b Sid -> Maybe (Sid,Sid)
test2 m = case (test1 id) of
MLeft x -> case m of
MRight y -> Just (x,y)
_ -> Nothing
_ -> Nothing
test3 :: MEither a b -> b
test3 (MRight x) = x
test4 = test3 (test1 id)
{-# OPTIONS_GHC -fglasgow-exts #-}
module Church1 where
-- Church numerals w/o extra type constructors
type CNat = forall a. (a->a) -> a -> a
n0 :: CNat
n0 = \f z -> z
n1 :: CNat
n1 = \f z -> f z
nsucc :: CNat -> CNat
nsucc n = \f z -> f (n f z)
add, mul :: CNat -> CNat -> CNat
add m n = \f -> \a -> m f (n f a)
mul m n = \f -> \a -> m (n f) a
-- already works with GHC 6.4
exp0 :: CNat -> CNat -> CNat
exp0 m n = n m
exp1 :: CNat -> CNat -> CNat
exp1 m n = (n::((CNat -> CNat) -> CNat -> CNat)) (mul m) n1 -- checks with app rule
{-# OPTIONS_GHC -fglasgow-exts #-}
module Church2 where
-- Church numerals w/o extra type constructors: Should fail
type CNat = forall a. (a->a) -> a -> a
n0 :: CNat
n0 = \f z -> z
n1 :: CNat
n1 = \f z -> f z
nsucc :: CNat -> CNat
nsucc n = \f z -> f (n f z)
add, mul :: CNat -> CNat -> CNat
add m n = \f -> \a -> m f (n f a)
mul m n = \f -> \a -> m (n f) a
-- already works with GHC 6.4
exp0 :: CNat -> CNat -> CNat
exp0 m n = n m
-- should fail!
exp2 :: CNat -> CNat -> CNat
exp2 m n = n (mul m) n1
TOP=../../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/test.mk
{-# OPTIONS_GHC -fglasgow-exts #-}
module PList1 where
-- Polymorphic lists 1: requires smart-app-res
type Sid = forall a . a -> a
ids :: [Sid]
ids = []
-- requires smart-app-res
test0 :: [Sid]
test0 = (\x->x) : ids
test1 :: [Sid] -- SLPJ added
test1 = ids ++ test0
test2 :: [Sid]
test2 = tail test1
test3 :: [Sid] -- SLPJ added
test3 = reverse test2
test4 = (tail::([Sid]->[Sid])) test2
test5 = (head::([Sid]->Sid)) test2
\ No newline at end of file
{-# OPTIONS_GHC -fglasgow-exts #-}
module PList2 where
-- Polymorphic lists 2: require smart-app-arg & smart-app-res: Should fail w/o smart-app-arg
type Sid = forall a. a -> a
ids :: [Sid]
ids = []
test0 :: [Sid]
test0 = (\x -> x):ids -- requires smart-app-res
test1 :: [Sid] -- Added SLPJ
test1 = ids ++ test0
test2 :: [Sid]
test2 = tail test1 -- requires smart-app-arg
test3 :: [Sid] -- Added SLPJ
test3 = reverse test2
test4 :: Sid
test4 = head ids --requires smart-app-arg
test5 :: Sid
test5 = head ids -- still requires smart-app-arg
{-# OPTIONS_GHC -fglasgow-exts #-}
module SystemF where
-- System-F examples
type Sid = forall a. a -> a
apply :: forall a b . (a -> b) -> a -> b
apply f g = f g
hr :: (forall a. a -> a) -> (Int,Bool)
hr f = (f 3,f True)
test0 = apply hr id -- requires smart-app-arg
selfApp :: Sid -> Sid
selfApp x = (x::(Sid -> Sid)) x
# Boxy-type tests
# test('Base1', normal, compile, [''])
# test('Church1', normal, compile, [''])
# test('Church2', normal, compile_fail, [''])
# test('PList1', normal, compile, [''])
# test('Plist2', normal, compile, [''])
# test('SystemF', normal, compile, [''])
# test('boxy', normal, compile, [''])
{-# OPTIONS_GHC -fglasgow-exts #-}
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)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment