module X {
sig x : t1
val x = e1
val y = e2
}
The principal signature of X is { val x : t1 } instead of the
expected {val x : t1; val y : t2 }. This is because principal
signature computation for a structure looks for sig f : t
declarations. Type elaboration should insert such declarations.
This will require a slight architectural tweak. Currently that
portion of the typechecking code assumes that each field
declaration in the structure before typechecking gives rise to
exactly one field declaration after typechecking (it uses a list of
decls for the module and just conses the fields together). Instead
we should use a Endo [Decl] Monoid to allow zero or more elaborated
declarations.
At the very least :: vs : in type ascription.
file:src/Insomnia/SurfaceSyntax/ToAST.hs::– TODO: allow models to contain parameters
model X {
parameter p = e
val s ~ e'
}
-- becomes
module X {
parameter p = e
model $Model {
val s ~ e'
}
}
-- in the rest of the program, references to X as a model now go to X.$Model
-- note that X.s is not legal, so it's only things like sampling from X or observing it.
- CLOSING NOTE [2015-09-18 Fri 11:56]
(Translating to FOmega instead, and interpreting that.)
file:src/Insomnia/Interp/ToLam.hs::– TODO: translate models
file:src/Insomnia/SurfaceSyntax/Parse.hs::– TODO: use the type
Specifically, “->” ought to live somewhere. file:src/Insomnia/SurfaceSyntax/ToAST.hs::– TODO: these really ought to be imported from somewhere, not built in.
file:src/Insomnia/SurfaceSyntax/ToAST.hs::– TODO: make infix resolution tests executable again.file:src/Insomnia/Toplevel.hs::– TODO: worth representing this stuff using Unbound binders?
file:src/Insomnia/Typecheck/ClarifySignature.hs::– TODO: share the value constructors of a generative type definition. file:src/Insomnia/Typecheck/ClarifySignature.hs::– TODO: also need to alias the value constructors. Will need a This is probably not too difficult internally now since value constructors are a separate datatype.
file:src/Insomnia/Typecheck/Env.hs::– TODO: the rest of the env
file:src/Insomnia/Typecheck/Expr.hs::– XXX : TODO generalize uvars, or else freeze ‘em if we’re going to file:src/Insomnia/Typecheck/Module.hs::– XXX TODO: generalize here. Or else decree that
But maybe not. Folk wisdom is that programmers don’t mind putting in type annotations for truly polymorphic local bindings.
The story is dodgier for toplevel bindings, but perhaps it’s okay for these also to require a signature.
file:src/Insomnia/Typecheck/ModuleType.hs::– TODO: actually check that the field names are unique.
file:src/Insomnia/Types.hs::data Rows = Rows – TODO
Parse to full application, understand fixity declarations, parse with precedence to disambiguate applications.
Use exact rationals for precedence, not integers!
forall i : t1 in f i ~ e i
Unless they turn out to be useful, in which case we will need to understand their semantics.
case e of
{ f1 = p1, f2 = p2 } -> e
The parser sees the above as an explicitly-delimited pattern list. case e of { pat1 ; pat2 }.
So we get a parse error about the leftmost =.
The workaround is to write
case e of
({ f1 = p1, f2 = p2 }) -> e
If bare record types (without a datatype wrapped around them) are going to be common, this may get very annoying.
Assuming that we can lexically distinguish values, constructors and operators, we should have a better representation of fixity declarations in the ToAST module. file:src/Insomnia/SurfaceSyntax/ToAST.hs::– TODO: this is horrible. rethink how we resolve associativity and precedence. file:src/Insomnia/SurfaceSyntax/ToAST.hs::– TODO: we should handle default fixity in a more principled way.
http://ppaml.cs.tufts.edu/Sean%E2%80%99s%20simple%20model%20notation
sbs: It would be helpful to separate the model from the query form and from the definitions of the observations.
– this is a big joint distribution (with some kinda ML-module like – dependent record type) called “T”
dist T is N ∷ ℕ type classes ∷ enum N
- mu’ ∷ ℝ
- σ’ ∷ ℝ⁺
M ∷ ℕ type object ∷ enum M class ∷ object → classes awesomeness ∷ object → ℝ mu ∷ classes → ℝ σ ∷ classes → ℝ⁺
the model gives the joint distribution over this type. there might be nuisance variables that noone will condition or query on.
this might be the model type. And we may want to mark μ’ and σ’ distinctly since they will not be exposed from the model type.
This is akin to a ML module.
There is a step here (not yet shown) to turn it into a conditional distribution.
Two observation forms:
observe (P :: T → Bool) :: (Dist T → Dist T)
observe v (where v is a value (of type T?) for some restricted set of types T. Maybe just polynomials of Int and Real)
Actually the idea is more like a type-directed operator “observe τ” where τ is the type of some path into a model. Given by a judgment ⌜T⊢ τ → (a → Dist T → Dist T)⌝.
So the idea is if we have a model M with model type T, then if S is a super-type (dropped components) then something like “observable M S” means that we promise to only observe the S components.