← Back to branch summary

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

« back to all changes in this revision

Viewing changes to notes/talks/Modules/notes

  • 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/Modules/notes
1
 
 
2
 
Module system talk
3
 
------------------
4
 
 
5
 
Purpose of the talk:
6
 
 
7
 
  - explain our module system
8
 
  - why we think it's good
9
 
  - get feedback
10
 
 
11
 
Important points:
12
 
 
13
 
  - talk about implementation
14
 
 
15
 
Outline
16
 
 
17
 
  - explain the idea
18
 
    + simple
19
 
    + separate scope checking and type checking
20
 
 
21
 
  - describe the module system (simplified?)
22
 
    + features
23
 
      - open
24
 
      - using/hiding/renaming
25
 
      - abstract/private
26
 
      - parameterised modules
27
 
      - separate typechecking
28
 
    + use examples
29
 
 
30
 
  - describe the implementation
31
 
    + scope checking
32
 
    + the view of the type checker
33
 
 
34
 
  - demo (the prototype)
35
 
    + look at the result of scope checking
36
 
    + look at the result of type checking
37
 
 
38
 
  - Agda 2 demo
39
 
    + look at a real example
40
 
 
41
 
Before scope checking:
42
 
 
43
 
  Unmodified source program (local names, hierarchical modules)
44
 
 
45
 
After scope checking:
46
 
 
47
 
  Fully qualified names
48
 
    - A.B.C.f
49
 
    - A.B.x
50
 
 
51
 
  Still hierarchical module structure
52
 
 
53
 
  How does it work?
54
 
    - keeps track of renamings
55
 
    - basically keeps a map from local name to fully qualified name
56
 
 
57
 
  Maybe scope checking should flatten the module space? No, instantiating a
58
 
  module would be a problem then. Or would it? We already perform all kinds of
59
 
  tricks when instantiating modules. Let's try.
60
 
 
61
 
After type checking
62
 
 
63
 
  Flat module structure
64
 
    - A.B.C -> { f, g, h }
65
 
    - A.B   -> { x, y }
66
 
 
67
 
Flatten modules at scope checking
68
 
---------------------------------
69
 
 
70
 
  What do we need to keep?
71
 
  - parameterised modules (to avoid re-type checking parameters)
72
 
  - module instantiations
73
 
 
74
 
  So something like:
75
 
 
76
 
  Given
77
 
 
78
 
    module A Δ where
79
 
      f : A
80
 
      g : B
81
 
 
82
 
    module B Γ = A t
83
 
 
84
 
  scope checking yields
85
 
 
86
 
    section Δ
87
 
      A.f : A
88
 
 
89
 
    module B Γ = A t
90
 
 
91
 
  and type checking then produces
92
 
 
93
 
    A { f : Δ -> A }
94
 
    B { f : Γ -> A[t/Δ] }
95
 
 
96
 
  type checking a section is very simple (just abstract the telescope)
97
 
 
98
 
  type checking a module instantiation of A will instantiate all modules with
99
 
  prefix A (A, A.M.P, ..)
100
 
 
101
 
How does renaming work at the moment?
102
 
-------------------------------------
103
 
 
104
 
  - it's completely ignore at type checking
105
 
 
106
 
 vim: sts=2 sw=2 tw=80