haskell/UniversalQuantification.hs at master · GollyTicker/haskell · GitHub

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
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-}

-- http://stackoverflow.com/questions/3071136/what-does-the-forall-keyword-in-haskell-ghc-do
-- playing with universal quantification

import Data.Typeable
import Text.Printf

f :: forall a. a -> a
f = id


-- ScopedTypeBariables
rfold :: forall a b. (a -> b -> b) -> b -> [a] -> b
rfold f z ls = go ls
    where
        go :: [a] -> b
        go [] = z
        go (x:xs) = f x (go xs)
{-
> rfold ((++). show) "" [1,2,3]
"123"
-}

-- RankNTypes
onBoth :: (forall a. a -> f a) -> (a, b) -> (f a, f b)
onBoth f (a,b) = (f a, f b)

{-
> onBoth (:[]) ("sdf", 4)
(["sdf"],[4])

onBoth (Just) ("sdf", 4)
(Just "sdf",Just 4)
-}


-- ExistentialQuantification

data Constraint = forall a. Eq a => Binary (a -> a -> Bool) a a

apply :: Constraint -> Bool
apply (Binary f a b) = f a b

cons :: Constraint
cons = Binary (==) 5 5

zwei :: Constraint
zwei = Binary (/=) 'c' 'd'

compare :: Constraint -> Constraint -> Bool
compare a b = apply a == apply b

mylist = [
        Binary (==) 5 5, Binary (==) 5 6,
        Binary (/=) 'c' 'd', Binary (/=) 'c' 'c'
     ]


-- ImpredicativeTypes
data Bi = forall a. Typeable a =>
            Bi
                String -- name der funktion
                -- constraintvergleichfunktion
                (forall b c. (Typeable b, Typeable c) => b -> c -> Bool)
                (a -> a -> Bool) -- originale Funktion

instance Show Bi where show (Bi s _ _) = s

list :: [Bi]
list = [
    mkConstraint "eq"  ( (==) :: Char   -> Char     -> Bool ),
    mkConstraint "neq" ( (/=) :: String -> String   -> Bool ),
    mkConstraint "lt"  (  (<) :: Int    -> Int      -> Bool )
    ]

mkConstraint :: Typeable a => String -> (a -> a -> Bool) -> Bi
mkConstraint s f = Bi s (generalize f) f

a :: Bi
a = Bi "" (generalize eqInt) eqInt
    where eqInt :: (Int -> Int -> Bool)
          eqInt = (==)

-- typeconvert from any type and test
generalize ::
    (Typeable a, Typeable b, Typeable c) =>
    (a -> a -> Bool)
    -> b -> c -> Bool
generalize f b c = case (cast b, cast c) of
        (Just a, Just a') -> f a a'
        _ -> True

-- typeconvert to int and test
ss :: Typeable b =>  (Int -> Int -> Bool) -> b -> b -> Bool
ss f tb tb' = case (cast tb, cast tb') of
            (Just a, Just a') -> f a a'
            _ -> False

data Elem = forall a. (Show a, Typeable a) => Elem a

instance Show Elem where show (Elem a) = show a

ls :: [Elem]
ls = [Elem (5::Int), Elem "sdf", Elem 'c', Elem "s", Elem (6::Int)]


pairs :: [Elem] -> [Bi] -> (Elem -> Elem -> Bi -> a) -> [a]
pairs ls cons f = [f x y c | x <- ls, y <- ls, c <- cons]

main :: IO ()
main = mapM_ print results
    where
        results = pairs ls list f
        f :: Elem -> Elem -> Bi -> String
        f (Elem a) (Elem b) (Bi s c g) =
            show a ++ " " ++ s ++ " " ++ show b ++ " => " ++ show (c a b)