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