Edward Z. Yang wrote:
1. I can't tell what arguments are implicit and which are explicit.
My first intuition is that things with triple colons are implicit,
but it turns out Urweb can infer a bit more than I thought, and
I have a really hard time judging it.
Without any explicit overriding of implict-ness, the only implicit
arguments are (a) constructor (type-level) arguments with [:::] in their
type portions, (b) type class witnesses, and (c) folders.
For example, I think I
want to use Variant.destrR. Which arguments do I need to pass
it, which do I not? The rampant use of un-inferred application (@)
makes that harder.
I _think_ the above explanation (which is also lurking somewhere in the
manual) says exactly which arguments are required. Note (also as
explained in the manual) that [@] switches to explicit passing of type
class witnesses and folders, but leaves constructor (i.e., type-level)
arguments implicit. You use [@@] to make all three categories explicit.
2. As a relative novice to metaprogramming in general, my understanding is
definitions tend to be hard to read and write, but easy to use (this is
in
contrast to value level computation, where looking at the body tells me
basically what a function does.) But there are no docs, usage or
otherwise, for most of the combinators in the metaprogramming libraries.
This impedes understanding.
To me, the types more or less explain what the functions must do, thanks
to "theorems for free"! And then the function names add a bit more of a
nudge, in cases with some ambiguity.
Do you have a question about a particular function that I might be able
to explain?
3. Each level of the type system (kinds, types, values) has its own
syntax, and while this is not necessarily a bad thing it makes
it a bit more complicated to assess what is what, being unfamiliar
with the syntax. The fact that the grammar given in the manual
uses Unicode symbols and not ASCII symbols exacerbates the problem.
(Do we have an ASCII grammar lying aruond somewhere?)
The closest thing to an ASCII grammar right now is src/urweb.lex and
src/urweb.grm, unfortunately. The list of ASCII-to-LaTeX mappings is
pretty small, so I hope it doesn't take long to internalize, and then
the grammar in the manual should be straightforward to interpret.
Now, for the particular problem I'm trying to figure out: I'm writing the
ToJson method for the json_variant typeclass:
fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts))
(names : $(map (fn _ => string) ts)) : json (variant ts) =
I am given a value of type (variant ts). This variant has a string name
associated
with it in names, and the inside json typeclass to call for the inner data in
jss.
So what I would like to do is use variant to "destruct" jss and names, gaining
access to a string (the name of the variant) and the appropriate typeclass
object for the inner data, and access to the inside data of the
variant (with these two types unified appropriately.)
OK. What do I want? How do I start? Do I want destructR? It doesn't seem
to have quite the right signature.
All of the specific functions like those in [Variant] are defined in the
end in terms of [fold], which comes from [Top], a module that is open by
default in all Ur programs. I think it's a nice down-the-rabbit-hole
exercise to understand how to build up the tower of helpful functions,
starting just from [fold]; but of course you will want to avoid that
when possible. :)
It looks to me like, for the [ToJson] part, you would ideally use a
close variation of [Variant.destrR]. In particular, you want a function
that takes one variant and two records, instead of one variant and one
record. Does it make sense that this is the key missing piece? Do you
see how to implement it? I think it can be done without any new folding
by combining [Variant.destrR] and [map2] (from [Top], though you don't
need to qualify it as such to use it).
For the [FromJson] direction, I don't see a direct match with an
existing fold function. Intuitively, you want to fold over [jss] and
[names], building a function that checks if the current name is in the
JSON record syntax, and, if so, uses the current element of [jss] to
parse the data. (This is all modulo character-level decomposition of
the string, which can be done as demonstrated in [json_record], though
it may be easier for variant encodings of fixed JSON record size.) The
folding over two records part can be done with [foldR2] from [Top], but
I don't see a way to avoid some manual manipulation of variants without
writing new code. (Though I can see [Variant.weaken] being useful to
support a simple choice of accumulator type in the fold.)
I believe knowledge of how to accomplish the above tasks will follow
from an understanding of the types of the different fold-based
functions, starting with the most basic [fold], so please fire away with
questions about them!
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
