blob: f0a55bdd42285e03d272e917e40df4d140ad9136 (
plain)
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
|
(.module:
[library
[lux "*"
[abstract
[functor {"+" [Functor]}]
[apply {"+" [Apply]}]
[monad {"+" [Monad]}]]
[type
abstract]]])
(abstract: .public (Policy brand value label)
value
[(type: .public (Can_Upgrade brand label value)
(-> value (Policy brand value label)))
(type: .public (Can_Downgrade brand label value)
(-> (Policy brand value label) value))
(type: .public (Privilege brand label)
(Record
[#can_upgrade (Can_Upgrade brand label)
#can_downgrade (Can_Downgrade brand label)]))
(type: .public (Delegation brand from to)
(All (_ value)
(-> (Policy brand value from)
(Policy brand value to))))
(def: .public (delegation downgrade upgrade)
(All (_ brand from to)
(-> (Can_Downgrade brand from) (Can_Upgrade brand to)
(Delegation brand from to)))
(|>> downgrade upgrade))
(type: .public (Context brand scope label)
(-> (Privilege brand label)
(scope label)))
(def: privilege
Privilege
[#can_upgrade (|>> :abstraction)
#can_downgrade (|>> :representation)])
(def: .public (with_policy context)
(All (_ brand scope)
(Ex (_ label)
(-> (Context brand scope label)
(scope label))))
(context ..privilege))
(def: (of_policy constructor)
(-> Type Type)
(type (All (_ brand label)
(constructor (All (_ value) (Policy brand value label))))))
(implementation: .public functor
(:~ (..of_policy Functor))
(def: (each f fa)
(|> fa :representation f :abstraction)))
(implementation: .public apply
(:~ (..of_policy Apply))
(def: &functor ..functor)
(def: (on fa ff)
(:abstraction ((:representation ff) (:representation fa)))))
(implementation: .public monad
(:~ (..of_policy Monad))
(def: &functor ..functor)
(def: in (|>> :abstraction))
(def: conjoint (|>> :representation)))]
)
(template [<brand> <value> <upgrade> <downgrade>]
[(abstract: .public <brand>
Any
[(type: .public <value>
(Policy <brand>))
(type: .public <upgrade>
(Can_Upgrade <brand>))
(type: .public <downgrade>
(Can_Downgrade <brand>))]
)]
[Privacy Private Can_Conceal Can_Reveal]
[Safety Safe Can_Trust Can_Distrust]
)
|
