Hi Igor,
> Now I've found my main problem with epigram papers: too many unknown
> terms. There are several kinds of arrows (in View From The Left) and I'm not
> sure what means
> => illustrative purposes, not element of Epigram ?
ASCII version of
> |-> Epigram syntax ("return" or "by")
meaning return the value of the expression right of the arrow
"by" is '<=' followed by 'case','rec' or 'view' and the variable you want to
analyse
> ~> type coercion, code transformation, etc ?
think 'eval'
> |- inferred by typesystem's logic ?
used for stating that a typing (right of |-) holds in the context given left of
the turnstile
> ||- the same as above ?
yes but now for labelled types, about which you don't have to care much when
you're programming since epigram uses these in the background to aid the
programming process. How epigram engages dependent types itself.
> |> elaborated as (what is it?)
> ---------------- below this line is logically derived from above this
> line ?
Gentzen style inference system. Used to give the rules of the typing relation.
But as 'The view from the left' introduces the design of epigram i recommend
you to read the epigram tutorial
http://www.cs.nott.ac.uk/~ctm/epigram-notes.ps.gz as well where
⎛ ⎞ ⎡ ⎤
∗ ∀ λ → ⋀ ⇒ ⇐ ⎝ ⎠ ⎣ ⎦ ────
* all lam -> /\ => <= ( ! [ ! ---
! ) ! ]
suffices as the main syntax reference.
> And what is "eliminator"? What is it supposed to do?
To get anywhere from a programs input in type theory you have to invoke an
eliminator specific to the inputs type on it. Examples are:
pair: projection
enumeration: case analysis
function: application
number: induction
By the way, how the epigram system uses eliminators pretty much gives you what
you once asked for on the curry mailling list:
http://www.informatik.uni-kiel.de/~mh/curry/listarchive/0305.html
namely to instantiate a variable from type information alone.
Just for the fun of it i used Sergio Antoys solution
http://www.informatik.uni-kiel.de/~mh/curry/listarchive/0309.html
to write some scopedness and typedness constraints on suitable representation
of terms found in the epigram tutorial:
http://www.informatik.uni-kiel.de/~seha/scpdnss.curry
http://www.informatik.uni-kiel.de/~seha/tpdnss.curry
Alas, this is 'faking it' stuff as these constraints don't feed any more
information to the compiler.
And i should make clear, that invoking eliminators in epigram happens during
elaboration to make sure you write exhaustive pattern matching programs and not
to patch free variables with constructor forms at runtime.
Best regards,
Sebastian
