Functor.hascasl.output revision 5de34eba726f63d1522bf17a857309a6208ce0b5
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
vars a, b, c : Type; x : a; f : a -> b; g : b -> c
ops __comp__ : (b -> c) * (a -> b) -> a -> c;
id : a -> a
. id x = x
. (g comp f) x = g (f x);
class Functor < Type -> Type
{vars a, b, c : Type; F : Functor; f : a -> b; g : b -> c
op map : (a -> b) -> F a -> F b
. map id = (id : F a -> F a)
. (map (g comp f) : F a -> F c) = map g comp map f;
}
class PolyFunctor < Functor
class PolyBifunctor < Type -> PolyFunctor
vars F : Functor; a, b : Type
type Alg F a := F a -> a
op __::__->__ : Pred ((a -> b) * (Alg F a) * (Alg F b))
class DTFunctor < Functor
{vars F : DTFunctor; a : Type
type InitialCarrier F
ops initialAlg : Alg F (InitialCarrier F);
fold : Alg F a -> InitialCarrier F -> a
vars alpha : Alg F a; g : InitialCarrier F -> a
. g :: initialAlg -> alpha <=> g = fold alpha;
}
class PolyFunctor < DTFunctor
var G : PolyBifunctor
type ParamDT G a := InitialCarrier (G a)
type ParamDT G : DTFunctor
vars l : ParamDT G a; f : a -> a
classes
DTFunctor < Type -> Type;
Functor < Type -> Type;
PolyBifunctor < Type -> Type -> Type;
PolyFunctor < Type -> Type
classes
DTFunctor < Functor;
PolyBifunctor < Type -> PolyFunctor;
PolyFunctor < DTFunctor
types
Alg : Functor -> Type -> Type;
InitialCarrier : DTFunctor -> Type;
ParamDT : PolyBifunctor -> DTFunctor
types
Alg (F : Functor) (a : Type) := F a -> a;
ParamDT (G : PolyBifunctor) (a : Type) := InitialCarrier (G a)
vars
F : DTFunctor %(var_59)%;
G : PolyBifunctor %(var_75)%;
a : Type %(var_60)%;
b : Type %(var_56)%;
c : Type %(var_12)%
op __::__->__ : forall F : Functor; a : Type; b : Type
. Pred ((a -> b) * Alg F a * Alg F b)
op __comp__ : forall a : Type; b : Type; c : Type
. (b -> c) * (a -> b) -> a -> c
op fold : forall F : DTFunctor; a : Type
. Alg F a -> InitialCarrier F -> a
op id : forall a : Type . a -> a
op initialAlg : forall F : DTFunctor . Alg F (InitialCarrier F)
op map : forall a : Type; b : Type; F : Functor
. (a -> b) -> F a -> F b
vars
alpha : Alg F a;
f : a -> a;
g : InitialCarrier F -> a;
l : ParamDT G a;
x : a
forall a : Type; x : a . id x = x
forall a : Type; b : Type; c : Type; f : a -> b; g : b -> c; x : a
. (g comp f) x = g (f x)
forall F : Functor; a : Type . map id = (id : F a -> F a)
forall
F : Functor; a : Type; b : Type; c : Type; f : a -> b; g : b -> c
. (map (g comp f) : F a -> F c) = map g comp map f
forall
F : DTFunctor; a : Type; alpha : Alg F a; g : InitialCarrier F -> a
. g :: initialAlg -> alpha <=> g = fold alpha
1.6: ### Hint: is type variable 'a'
1.8: ### Hint: is type variable 'b'
1.10: ### Hint: is type variable 'c'
1.20: ### Hint: not a class 'a'
1.26: ### Hint: not a class 'a'
1.26: ### Hint: not a class 'b'
1.37: ### Hint: not a class 'b'
1.37: ### Hint: not a class 'c'
2.18-2.23: ### Hint:
no kind found for 'b -> c'
expected: {Cpo}
found: {Type}
2.18-2.23: ### Hint:
no kind found for 'b -> c'
expected: {Cppo}
found: {Type}
8.7: ### Hint: is type variable 'a'
8.7: ### Hint: rebound type variable 'a'
8.9: ### Hint: is type variable 'b'
8.9: ### Hint: rebound type variable 'b'
8.11: ### Hint: is type variable 'c'
8.11: ### Hint: rebound type variable 'c'
8.20: ### Hint: is type variable 'F'
8.33: ### Hint: not a class 'a'
8.33: ### Hint: not a class 'b'
8.32: ### Hint: rebound variable 'f'
8.44: ### Hint: not a class 'b'
8.44: ### Hint: not a class 'c'
8.43: ### Hint: rebound variable 'g'
16.5: ### Hint: is type variable 'F'
16.5: ### Hint: rebound type variable 'F'
16.17: ### Hint: is type variable 'a'
16.17: ### Hint: rebound type variable 'a'
16.19: ### Hint: is type variable 'b'
16.19: ### Hint: rebound type variable 'b'
18.23-18.28: ### Hint:
no kind found for 'a -> b'
expected: {Cpo}
found: {Type}
18.23-18.28: ### Hint:
no kind found for 'a -> b'
expected: {Cppo}
found: {Type}
21.5: ### Hint: is type variable 'F'
21.5: ### Hint: rebound type variable 'F'
21.19: ### Hint: is type variable 'a'
21.19: ### Hint: rebound type variable 'a'
25.10: ### Hint: not a kind 'Alg F a'
25.22: ### Hint: not a kind 'InitialCarrier F -> a'
25.21: ### Hint: rebound variable 'g'
28.7-28.17: ### Warning: refined class 'PolyFunctor'
29.5: ### Hint: is type variable 'G'
33.7: ### Hint: not a kind 'ParamDT G a'
33.23: ### Hint: not a class 'a'
33.23: ### Hint: not a class 'a'
33.22: ### Hint: rebound variable 'f'
34.9: ### Hint:
in type of '(var l : ParamDT G a)'
type 'InitialCarrier' (30.21)
is not unifiable with differently kinded type '_v82_F' (9.21)
34.9: ### Hint: untypeable term (with type: _v82_F _v80_a) 'l'
34.3-34.29: ### Hint:
untypeable term (with type: ? _v79_a * ? _v79_a)
'(map f l, fold initialAlg l)'
34.11: *** Error: no typing for 'map f l = fold initialAlg l'