Here are some good remarks from people listening to the talk.
Catarina:
How will you distinguish between record projection and module projection
when you add records?
Good question. One option is to use a different syntax for record
projection. For instance, p!x.
Conor:
We won't be able to satisfy all equations of Berry's majority function
definitionally in the core language, so if we do that in the full
language we are in trouble.
maj T T T = T
maj T F x = x
maj F x T = x
maj x T F = x
maj F F F = F
Possible solution: Match patterns left-to-right, as soon as there is an
inconclusive match the whole matching is inconclusive. Example:
f T F = F
f _ _ = T
With the standard approach we have
f x T --> T
but instead we say that this doesn't reduce (since x is blocking the
pattern T in the first clause). With this approach order does matter! Are
there any problems? Example:
f x 0 = 1
f 0 (s y) = y
f (s x) (s y) = x
With left to right matching we still have f x 0 --> 1, but the
tranlation will yield(?)
f 0 = \y -> f1 y
f (s x) = \y -> f2 x y
f1 0 = 0
f1 (s y) = y
f2 x 0 = 1
f2 x (s y) = x
That is pattern matching first on the first argument. So f x 0 will not
reduce. Hm.
Makoto:
When lifting local definitions you might not want to abstract over all
variables in the context, but only those which are in scope. Example:
foo x y z = bar y
where
bar true = true
bar false = z
Abstracting over all variables gives the following:
lift_bar x y z true = true
lift_bar x y z false = z
foo x y z --> lift_bar x y z y
foo x' y z --> lift_bar x' y z y
So foo x y z != foo x' y z, even though foo never uses its first
argument. If we instead abstract only over things that are actually used
we get:
lift_bar z true = true
lift_bar z false = z
foo x y z --> lift_bar y z
foo x' y z --> lift_bar y z
Andreas:
Would it be possible to add rewriting rules for definitional equalities which
hold inside a module (where we know the values of abstract things) when
working outside the module?
Example:
module Stack where
abstract
Stack : Set -> Set
Stack = List
push : A -> Stack A -> Stack A
push = cons
pop : Stack A -> Maybe (Stack A)
pop nil = nothing
pop (x::xs) = just xs
rewrite pop (push x s) == just s
The type of the rewrite should be checked without knowing the definitions
and the left-hand-side and the right-hand-side should be convertible when
knowing the definitions.
Conor:
It would be nice to have a parameterised module containing all the local
definitions for each definition. This way you could actually refer to the
local functions by instantiating this module.
f : (x:A) -> (y:B) -> C
f x y = e
where
g : (z:C) -> D
g z = e'
would mean something like
module f (x:A)(y:B) where
g : (z:C) -> D
g z = e'
f : (x:A) -> (y:B) -> C
f x y = e
where
module Local = f x y
open Local
Open problem: How to handle definitions with multiple clauses?
vim: sts=2 sw=2 tw=75