← Back to branch summary

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

« back to all changes in this revision

Viewing changes to notes/design/meeting_050906

  • 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/design/meeting_050906
1
 
 
2
 
Syntax - concrete, internal and values
3
 
--------------------------------------
4
 
 
5
 
  Nice syntax for hidden arguments:
6
 
 
7
 
    {x:A} -> B
8
 
    {A} -> B
9
 
    \{x:A} -> e
10
 
    \{x} y -> e
11
 
    {x:A}(y:B)
12
 
    e {e}
13
 
    {x, y : A, b : B} -> A
14
 
 
15
 
  Scope of telescope is only the right of the colon:
16
 
 
17
 
    id {A : Set} : A -> A
18
 
    id x = x, or
19
 
    id {A} x = x
20
 
 
21
 
    id {A : Set}(x : A) : A
22
 
    id x = x
23
 
 
24
 
  Value datatype
25
 
 
26
 
    data Value = Var Nat
27
 
               | App Value Value Hidden
28
 
               | Lam Type (Abs Value)
29
 
               | Lit Literal
30
 
               | Def Name
31
 
               | Meta MId
32
 
    data Type  = El Value Sort
33
 
               | Pi Type (Abs Type)
34
 
               | Sort Sort
35
 
               | Meta MId
36
 
    data Sort  = Prop | Set Nat
37
 
 
38
 
    data Abs a = Abs Name a
39
 
 
40
 
    Everything also has an explanation on it.
41
 
    Note: No sorts on metas.
42
 
 
43
 
    data Expl = InYourCode Range
44
 
              | DefinedAt Range   -- for variables/names
45
 
              | Expl :+: Expl
46
 
              | ...
47
 
 
48
 
  Very cool idea
49
 
 
50
 
    Have type checker return proof objects:
51
 
 
52
 
      inferType : Term -> TCM InferenceDerivation
53
 
 
54
 
    Purpose
55
 
      - give better error messages
56
 
 
57
 
    Possibilities
58
 
      - allow the user to explore the derivation to find an error
59
 
 
60
 
    First (bad) approximation:
61
 
 
62
 
      data InferenceDerivation = Inferred Value Type
63
 
 
64
 
    Add constructor (functions) for each judgement in the type system.
65
 
 
66
 
  User syntax
67
 
 
68
 
    A, e ::= x | e e | e {e} | λ αs -> e | λ Δ -> e
69
 
           | {A} -> A | A -> A | Δ -> A | Set | Prop | Seti
70
 
           | let Locals in e | e es of Bs | c | lit | ? | _
71
 
    
72
 
    α ::= x | {x}
73
 
    B ::= es -> e
74
 
    Δ ::= ε | (xs:A,..,xs:A)Δ | {xs:A,..,xs:A}Δ
75
 
 
76
 
    D ::= Local | Module | postulate xΔ:A .. xΔ:A | Prefix D
77
 
    Prefix ::= abstract | private
78
 
 
79
 
    Local ::= Def | Data | mutual Locals
80
 
 
81
 
    Data ::= data x Δ : A where
82
 
               c : A
83
 
               ...
84
 
               c : A
85
 
    
86
 
    Def ::= [ x Δ : A ]
87
 
            x ps = e
88
 
            ...
89
 
            x ps = e
90
 
 
91
 
    p ::= c ps | x | {p}
92
 
 
93
 
    Module ::= package x Δ where
94
 
                 Ds
95
 
 
96
 
? and _
97
 
-------
98
 
 
99
 
  ? means hole and _ means implicit argument style meta variable.
100
 
  No ? implies no _ in top level def (D). In other words _ in top level
101
 
  definitions should be solved locally. This means that when we do have
102
 
  open holes in a definition we should still take care to not make the _
103
 
  depend on things defined later on.
104
 
  Solution: if we get a constraint involving an _ from a previous
105
 
            definition, we report an error.
106
 
  
107
 
 
108
 
The State and Environment
109
 
-------------------------
110
 
 
111
 
  State
112
 
    - Meta variable stuff
113
 
    - Signature
114
 
 
115
 
  Environment
116
 
    - Context
117
 
 
118
 
  Signature
119
 
    - def -> type, def, fixity
120
 
    - data -> type, constructors, fixity
121
 
 
122
 
  Meta variable stuff
123
 
 
124
 
    - gensym (= Int)
125
 
 
126
 
    - instantiation:
127
 
        data MetaInfo = InstantiatedV Value
128
 
                      | InstantiatedT Type
129
 
                      | Underscore [ConstraintId]
130
 
                      | QuestionmarkV Context Type [ConstraintId]
131
 
                      | QuestionmarkT Context (Maybe Sort) [ConstraintId]
132
 
 
133
 
    - the stuff in the questionmarks correspond to the following
134
 
      constraints
135
 
        Γ ⊢ ? : V
136
 
        Γ ⊢ ? type^i  -- sometimes we care (? in type of constructor)
137
 
        Γ ⊢ ? type    -- and sometimes we don't (? in type of definition)
138
 
 
139
 
    - constraints: 
140
 
 
141
 
        Γ ⊢ v = w : V
142
 
        Γ ⊢ V = W
143
 
      
144
 
      also need Σ everywhere.
145
 
 
146
 
Cool interactions
147
 
-----------------
148
 
 
149
 
  * Abstract over uninstantiated questionmarks (without constraints).
150
 
  * Select things (names?) and do things
151
 
      - pattern match on pattern variable
152
 
          x + y = e  --{expand y}--> x + 0   = e[0/y]
153
 
                                     x + S y = e[S y/y]
154
 
      - what's my type
155
 
      - where's my definition/declaration
156
 
      - rename
157
 
  * Hide and unhide arguments.
158
 
 
159
 
vim: sts=2 sw=2 tw=75