Rosi/examples/Wand.ro at main · IowaFP/Rosi · GitHub

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
import Ro.Base

-- Examples
--
-- Comments are Haskell-style line comments

-- Example 1: Wand's example

-- Fully annotated

--   I am going to assume that:

--   prj : forall y z : R[*]. y < z => Pi z -> Pi y
--   (++) : forall x y z : R[*]. x + y ~ z => Pi x -> Pi y -> Pi z

--   inj : forall y z : R[*]. y < z => Sigma y -> Sigma z
--   (?) : forall x y z : R[*], t : *. x + y ~ z => (Sigma x -> t) -> (Sigma y -> t) -> Sigma z -> t

-- NB: the order of type arguments is not fixed by the existing formal developments!

-- Also, I am thinking that there is only infix support for primitives, and that
-- prefix versions of these will be encoded manually.

wand0 : forall x y z : R[*], t : *. x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
  -- Notes: label constants have an initial quote
  -- Records are `Pi z`; I guess variants are `Sigma z`.  (Unicode? still sucks for GHC on Windows)
wand0 = /\ x y z : R[*], t : *. \ m : Pi x, n : Pi y.
          prj [{'l := t}] [z] ((++) [x] [y] [z] m n) / 'l
  -- Not sure about punning singletons: Do we need to distinguish between the
  -- syntax for singleton #T and the type T?

-- Should be able to infer type arguments:

wand1 : forall x y z : R[*], t : *. x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
wand1 = /\ x y z : R[*], t : * . \ m : Pi x, n : Pi y.
          prj (m ++ n) / 'l

-- Should I be able to infer the presence of type abstractions from the type signature?
-- wand2 : forall x y z : R[*], t : *. x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
-- wand2 = \ m : Pi x, n : Pi y. prj (m ++ n) / #'l

-- Can infer types of function arguments:
wand3 : forall x y z : R[*], t : *. x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
wand3 = \ m n. prj (m ++ n) / 'l

-- Can infer kinds?

wand5 : forall x y z t. x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
wand5 = \ m n. prj (m ++ n) / 'l

-- Automatically generalize undeclared variables, in alphabetical order...

wand6 : x + y ~ z, {'l := t} < z => Pi x -> Pi y -> t
wand6 = \ m n. prj (m ++ n) / 'l

-- Have first-class labels

wand7 : x + y ~ z, {l := t} < z => #l -> Pi x -> Pi y -> t
wand7 = \l m n. prj (m ++ n) / l

-- And syntax for selection

wand8 : x + y ~ z, {l := t} < z => #l -> Pi x -> Pi y -> t
wand8 = \l m n. (m ++ n).l

-- And syntax for plusses...

wand9 : {l := t} < x + y => #l -> Pi x -> Pi y -> t
wand9 = \l m n. (m ++ n).l

-- Let's dualize the above

dnaw : x + y ~ z, {'l := t} < z => (Sigma x -> u) -> (Sigma y -> u) -> t -> u
dnaw = \ r s x. (r | s) ('l: x)

dnawHO : x + y ~ z, {'l := t} < z => (Sigma x u -> u) -> (Sigma y u -> u) -> t u -> u
dnawHO = \ f g x. (f | g) ('l: x)

dnaw1 : x + y ~ z, {l := t} < z => #l -> (Sigma x -> u) -> (Sigma y -> u) -> t -> u
dnaw1 = \l f g x. (f | g) (l: x)

dnaw2 : {l := t} < x + y => #l -> (Sigma x -> u) -> (Sigma y -> u) -> t -> u
dnaw2 = \l f g x. (f | g) (l: x)