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
|
module Encoded.Pair
import Encoded.Bool
import Encoded.Union
import Term.Syntax
export
(*) : Ty -> Ty -> Ty
ty1 * ty2 = B ~> (ty1 <+> ty2)
export
pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
pair = Abs $ Abs $ Abs $
let t = Var (There $ There Here) in
let u = Var (There Here) in
let b = Var Here in
App if' [<b, App inL [<t], App inR [<u]]
export
fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
fst = Abs $ App (prL . Var Here) [<True]
export
snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
snd = Abs $ App (prR . Var Here) [<False]
export
bimap :
{ty1, ty1', ty2, ty2' : Ty} ->
Term ((ty1 ~> ty1') ~> (ty2 ~> ty2') ~> ty1 * ty2 ~> ty1' * ty2') ctx
bimap = Abs $ Abs $ Abs $ Abs $
let f = Var (There $ There $ There Here) in
let g = Var (There $ There Here) in
let x = Var (There $ Here) in
let b = Var Here in
App if'
[<b
, App (inL . f . prL . x) [<True]
, App (inR . g . prR . x) [<False]
]
export
mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
mapSnd = Abs $ Abs $
let f = Var (There Here) in
let x = Var Here in
App pair [<App fst [<x], App (f . snd) [<x]]
export
uncurry : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty2 ~> ty) ~> ty1 * ty2 ~> ty) ctx
uncurry = Abs $ Abs $
let f = Var $ There Here in
let p = Var Here in
App f [<App fst [<p], App snd [<p]]
|
