question on overloading / simplification of types

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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
-- how can these two functions be given the same name with maximum type
-- inference?
f1 :: Double -> Double
f1 = succ

f2 :: Int -> Int -> Int
f2 = (+)

{- |

*Main> mptc 5 3
8

*Main> flex 5 3

<interactive>:9:1:
    Couldn't match type `a0 -> t0' with `Double'
    In the expression: flex 5 3
    In an equation for `it': it = flex 5 3
*Main> at 5 3

<interactive>:10:1:
    Couldn't match expected type `a1 -> t0' with actual type `ATT a0'
    The type variables `t0', `a0', `a1' are ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    The function `at' is applied to two arguments,
    but its type `a0 -> ATT a0' has only one
    In the expression: at 5 3
    In an equation for `it': it = at 5 3



*Main> mptc 5 :: Double
6.0

*Main> flex 5 :: Double
6.0

*Main> at 5 :: Double

<interactive>:14:1:
    Couldn't match expected type `Double' with actual type `ATT a0'
    The type variable `a0' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    In the return type of a call of `at'
    In the expression: at 5 :: Double
    In an equation for `it': it = at 5 :: Double


-- inferred types
*Main> :t mptc (2::Int)
mptc (2::Int) :: Int -> Int

*Main> :t flex (2::Int)
flex (2::Int) :: Flex (Int -> t) => t

*Main> :t at (2::Int)
at (2::Int) :: ATT Int


--
*Main> :t \x -> mptc x :: Double
\x -> mptc x :: Double :: Double -> Double

*Main> :t \x -> flex x :: Double
\x -> flex x :: Double :: Flex (t -> Double) => t -> Double

*Main> :t \x -> at x :: Double
\x -> at x :: Double :: (AT a, ATT a ~ Double) => a -> Double



-- this one could be improved:
*Main> :t \x y -> mptc x y :: Int
\x y -> mptc x y :: Int :: MPTC a (t -> Int) => a -> t -> Int



-}


-- * Flexible instances
{- | this is very poor:

*Main> :t flex 1 2

<interactive>:1:1: Warning:
    Couldn't match type `Integer -> t' with `Double'
    In the expression: flex 1 2
    flex 1 2 :: t

*Main> :t flex 1
flex 1 :: (Num a, Flex (a -> t)) => t


But sometimes it works:

*Main> flex 1 :: Double
2.0

*Main> flex 1 2  :: Int
3
-}
class Flex a where flex :: a
instance (a ~ Double, b ~ Double) => Flex (a -> b) where flex = f1
instance (a ~ Int, b ~ Int, c ~ Int) => Flex (a -> b -> c) where flex = f2


{- |

*Main> at (5 :: Double)
6.0

*Main> at 5 6 :: Int

<interactive>:21:1:
    Couldn't match expected type `a1 -> Int' with actual type `ATT a0'
    The type variables `a0', `a1' are ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    The function `at' is applied to two arguments,
    but its type `a0 -> ATT a0' has only one
    In the expression: at 5 6 :: Int
    In an equation for `it': it = at 5 6 :: Int

-}
class AT a where
    type ATT a
    at :: a -> ATT a

instance AT Double where
    type ATT Double = Double
    at = f1

instance AT Int where
    type ATT Int = Int -> Int
    at = f2

class AT2 a where
    type ATT2 a
    at2 :: ATT2 a -> a

instance AT2 Double where
    type ATT2 Double = Double
    at2 = f1

instance (a ~ b, b ~ Int) => AT2 (a -> b) where
    type ATT2 (a -> b) = Int
    at2 = f2

class MPTC a b | a -> b, b -> a where
    mptc :: a -> b

instance MPTC Double Double where mptc = f1
instance (b~ c, c~ Int) => MPTC Int (b -> c) where mptc = f2