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
|
%include poly.fmt
%if style == "newcode"
%format ^
%format ^^ = " "
%format ti(a) = "{|" a "|}"
%format ki(a) = "{[" a "]}"
%else
%format ^ = " "
%format ^^ = "\;"
%format ti(a) = "\lty " a "\rty "
%format ki(a) = "\lki " a "\rki "
\newcommand{\lty}{\mathopen{\{\mskip-3.4mu||}}
\newcommand{\rty}{\mathclose{||\mskip-3.4mu\}}}
\newcommand{\lki}{\mathopen{\{\mskip-3.5mu[}}
\newcommand{\rki}{\mathclose{]\mskip-3.5mu\}}}
%format t1
%format t2
%format a1
%format a2
%format r_ = "\rho "
%format s_ = "\sigma "
%format k_ = "\kappa "
%format forall a = "\forall " a
%format . = "."
%format mapa = map "_{" a "}"
%format mapb = map "_{" b "}"
%format :*: = "\times "
%endif
\begin{code}
type Map^ki(*) t1 t2 = t1 -> t2
type Map^ki(r_ -> s_) t1 t2 = forall a1 a2. Map^ki(r_) a1 a2
-> Map^ki(s_) (t1 a1) (t2 a2)
map^ti(t :: k_) :: Map^ki(k_) t t
map^ti(Unit) Unit = Unit
map^ti(Int) i = i
map^ti(Sum) mapa mapb (Inl a) = Inl (mapa a)
map^ti(Sum) mapa mapb (Inr b) = Inr (mapb b)
map^ti(Prod) mapa mapb (a :*: b) = mapa a :*: mapb b
\end{code}
|
