← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to notes/talks/video060510/remarks

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
notes/talks/video060510/remarks
1
 
 
2
 
Here are some good remarks from people listening to the talk.
3
 
 
4
 
Catarina:
5
 
 
6
 
  How will you distinguish between record projection and module projection
7
 
  when you add records?
8
 
 
9
 
  Good question. One option is to use a different syntax for record
10
 
  projection. For instance, p!x.
11
 
 
12
 
Conor:
13
 
 
14
 
  We won't be able to satisfy all equations of Berry's majority function
15
 
  definitionally in the core language, so if we do that in the full
16
 
  language we are in trouble.
17
 
 
18
 
    maj T T T = T
19
 
    maj T F x = x
20
 
    maj F x T = x
21
 
    maj x T F = x
22
 
    maj F F F = F
23
 
 
24
 
  Possible solution: Match patterns left-to-right, as soon as there is an
25
 
  inconclusive match the whole matching is inconclusive. Example:
26
 
 
27
 
    f T F = F
28
 
    f _ _ = T
29
 
 
30
 
  With the standard approach we have
31
 
 
32
 
    f x T --> T
33
 
 
34
 
  but instead we say that this doesn't reduce (since x is blocking the
35
 
  pattern T in the first clause). With this approach order does matter! Are
36
 
  there any problems? Example:
37
 
 
38
 
    f  x     0    = 1
39
 
    f  0    (s y) = y
40
 
    f (s x) (s y) = x
41
 
 
42
 
  With left to right matching we still have f x 0 --> 1, but the
43
 
  tranlation will yield(?)
44
 
 
45
 
    f 0     = \y -> f1 y
46
 
    f (s x) = \y -> f2 x y
47
 
 
48
 
    f1  0    = 0
49
 
    f1 (s y) = y
50
 
 
51
 
    f2 x  0    = 1
52
 
    f2 x (s y) = x
53
 
 
54
 
  That is pattern matching first on the first argument. So f x 0 will not
55
 
  reduce. Hm.
56
 
 
57
 
Makoto:
58
 
 
59
 
  When lifting local definitions you might not want to abstract over all
60
 
  variables in the context, but only those which are in scope. Example:
61
 
 
62
 
    foo x y z = bar y
63
 
      where
64
 
        bar true  = true
65
 
        bar false = z
66
 
 
67
 
  Abstracting over all variables gives the following:
68
 
 
69
 
    lift_bar x y z true  = true
70
 
    lift_bar x y z false = z
71
 
 
72
 
    foo x y z  --> lift_bar x  y z y
73
 
    foo x' y z --> lift_bar x' y z y
74
 
 
75
 
  So foo x y z != foo x' y z, even though foo never uses its first
76
 
  argument. If we instead abstract only over things that are actually used
77
 
  we get:
78
 
 
79
 
    lift_bar z true  = true
80
 
    lift_bar z false = z
81
 
 
82
 
    foo x y z  --> lift_bar y z
83
 
    foo x' y z --> lift_bar y z
84
 
 
85
 
Andreas:
86
 
 
87
 
  Would it be possible to add rewriting rules for definitional equalities which
88
 
  hold inside a module (where we know the values of abstract things) when
89
 
  working outside the module?
90
 
 
91
 
  Example:
92
 
 
93
 
    module Stack where
94
 
      abstract
95
 
        Stack : Set -> Set
96
 
        Stack = List
97
 
        push : A -> Stack A -> Stack A
98
 
        push = cons
99
 
        pop : Stack A -> Maybe (Stack A)
100
 
        pop nil = nothing
101
 
        pop (x::xs) = just xs
102
 
 
103
 
        rewrite pop (push x s) == just s
104
 
 
105
 
  The type of the rewrite should be checked without knowing the definitions
106
 
  and the left-hand-side and the right-hand-side should be convertible when
107
 
  knowing the definitions.
108
 
 
109
 
Conor:
110
 
 
111
 
  It would be nice to have a parameterised module containing all the local
112
 
  definitions for each definition. This way you could actually refer to the
113
 
  local functions by instantiating this module.
114
 
 
115
 
    f : (x:A) -> (y:B) -> C
116
 
    f x y = e
117
 
      where
118
 
        g : (z:C) -> D
119
 
        g z = e'
120
 
 
121
 
  would mean something like
122
 
 
123
 
    module f (x:A)(y:B) where
124
 
      g : (z:C) -> D
125
 
      g z = e'
126
 
 
127
 
    f : (x:A) -> (y:B) -> C
128
 
    f x y = e
129
 
      where
130
 
        module Local = f x y
131
 
        open Local
132
 
 
133
 
  Open problem: How to handle definitions with multiple clauses?
134
 
 
135
 
 vim: sts=2 sw=2 tw=75