agda/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