Agda-2.3.2.2: notes/thinkingAloud
Topic: Modules
Topic: Structure of the signature.
* The module system is hierarchical so it seems resonable to
structure the signature accordingly.
* We need to be able to look up a QName in the signature.
* Why does it have to be hierarchical? When do we need to manipulate
an entire subtree?
* A problem is that QNames aren't well thought out yet. Currently a
moduleId is a concrete name. That's not very good.
* Let's make it flat for the time being, that should be a simple
thing to change at a later stage.
* We would also have to think about what happens when modules are
instantiated (module Foo = Bar Nat), but that can also be
postponed.
EndTopic
Topic: Parameterised modules
* Turns out to be a major headache to keep track of free variables.
* We need to structure things nicely.
* Attempt 1: Hierarchical signature.
notes/ModulesAttempt1.hs
Not necessary(?)
* Attempt 2: Flat signature
notes/Modules.hs
EndTopic
Topic: Rewriting for abstract things
* Remark by Andreas during the video talk
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.
EndTopic
EndTopic
Topic: Local functions
Topic: Functions as parameterised modules
* Remark by Conor during the video talk
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?
EndTopic
Topic: Lifting
* Remark by Makoto during the video meeting
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
EndTopic
EndTopic
Topic: Pattern Matching
Topic: Berry's majority function
* Remark by Conor during the video talk:
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.
Can we figure out the correct order in which to pattern match?
Maybe. We can decide in which order to pattern match by scanning
the clauses left to right, top to bottom. The first constructor
pattern appears (in the example) in the second argument of the
first clause, so we should start by matching on the second
argument.
EndTopic
EndTopic
Topic: Meta variables
Topic: Meta variable dependencies and hidden application
* Currently meta variable dependencies are represented as
applications. This means that they contain hiding information.
* Is this a problem? It does clutter up some things, but on the
other hand it's possible that a meta variable _is_ applied to an
hidden argument.
EndTopic
Topic: Sort meta variables
* How can we solve them?
* When do we have to?
* One option could be to instantiate all unsolved (unconstrained)
sort metas to Set.
EndTopic
Topic: Dependency juggling
* Juggling parameters is a mess. There is a dire need for a nice
clean API.
EndTopic
Topic: Scope
* Meta variables need to be scope checked (probably) so when
creating a new meta we should have access to scope information.
It'll probably be enough to annotate declarations with scope and
make sure that the type checker updates the current scope when
passing a definition. Not having to bother with lambda bound
things makes it easier.
In any case interaction points need to have their scope. This we
have when type checking (and thus when creating the meta).
EndTopic
Topic: Question mark numbers
* We probably want to separate the numbers on question marks from
those on underscores.
* Possible solution:
- generate question mark numbers during scope checking
- generate MetaIds as before (both underscores and question marks)
- keep a map from question mark numbers to meta ids
- the interface will use question mark numbers
EndTopic
EndTopic
Topic: Implementation details
Topic: Representation
Topic: Unique names in abstract syntax.
* The names of local functions can clash and it's not clear how to
disambiguate them if names are (qualified) strings.
* So unique identifiers (numbers) for names sounds like a good idea.
* Problem: Module system, in particular separate type checking and
interface files. If names are identified by globally unique
numbers we're in trouble.
* Solution: qualified unique numbers. A name is a pair of a module
and a unique number.
* Question: How qualified (top-level modules or also sub-modules)?
* Answer: It feels better to treat top-level modules and sub-modules
the same as far as possible, so each module (including
sub-modules) should have its own set of unique identifiers.
EndTopic
Topic: Module names vs. function names
* Since there is no confusion between module names and function
names (they can never appear in the same place) it makes sense to
have different representations for them. For clarity if nothing
else.
EndTopic
Topic: n-ary application in terms.
* Some things might be simpler with binary application. Check it
out.
EndTopic
EndTopic
Topic: Generics
* How much do we gain by the generics? Is it worth it?
* Maybe there is a more light-weight approach.
EndTopic
Topic: Debugging
* How to make debugging smooth?
* We need different levels of information in print-outs.
EndTopic
Topic: Figuring out what's in Syntax.Internal(New)
* type Args = [Value]
* xxx2str :: xxx -> Reader Int String
Generates fresh names.
* Values can be beta redexes. Why? Maybe it will allow a better
reduction strategy than call-by-name. I'm not sure it matters.
* instance Eq Value. Only variables can be equal. Not very nice.
Make a type wrapper (or define another function).
* addArgs = flip apply (but generically)
* data Sort = ... | Lub Sort Sort -- do we need this?
* data TCErr = Fatal String | PatternErr MId
This is nice. Pattern unification failure might go away if we wait
a bit, PatternErr is used to signal such a failure.
* reduce is parameterised by the stuff that's in the monad. This
will probably make it more efficient than if it had been monadic.
We can do this since it'll never change the state.
EndTopic
Topic: Module structure of the type checker
- Syntax
- Internal
- TypeChecker
- TypeChecking/
- Conversion
- Reduce
- Monad
Where to put subst and adjust? Let's put them in Reduce for the time
being. No, that doesn't quite work. They'll have to go in
Substitute.
EndTopic
EndTopic
Topic: TODO
* Check that meta variables have been solved at appropriate times.
* Keep the type on instantiated interaction meta variables. Also
remember which metas are interaction points and which are go
figures after instantiation.
* Meta variable scope (see Meta variables - Scope).
EndTopic
vim: sts=2 sw=2 tw=70 fdm=marker foldmarker=Topic\:,EndTopic