Base1.hs 784 Bytes
Newer Older
1
{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
2

3 4
-- Sept 16: now failing, beause I've furter reduced the scop
--          of impredicative types
5

6 7 8 9 10
module Base1 where
-- basic examples of impredicative instantiation of variables

data MEither a b = MLeft a
                 | MRight b
11 12
                 | MEmpty

13
type Sid = forall a. a -> a
14

15 16
-- no need for impredicativity
test0 = MRight id
17

18
-- requires impredicativity
19
test1 :: Sid -> MEither Sid b
20
test1 fid = MLeft fid
21

22 23 24 25 26
test2 :: MEither b Sid -> Maybe (Sid,Sid)
test2 m = case (test1 id) of
             MLeft x -> case m of
                          MRight y -> Just (x,y)
                          _ -> Nothing
27 28 29
             _ -> Nothing

test3 :: MEither a b -> b
30
test3 (MRight x) = x
31

32
test4 = test3 (test1 id)
33