A fully-worked unqualifier example would be very helpful.

[adam-antonik]

I've been trying to make an Unqualifier, and find myself rather stuck.
Suppose I want to be able to write
a = foo :: (Foo "bar" w) => w
and have 'a' equal to the record {bar='bar'}
I need functions TString* -> MonoTypePtr and TString* -> ExprPtr which would seem to be something like

MonoTypePtr decodeStrType(const TString* tstr)
{
        return makeRecordType(tstr->value(), MonoTypePtr(Array::make(Prim::make("char"))));
}

ExprPtr decodeStrValue(const TString* tstr)
{
        LexicalAnnotation la;
        MkRecord::FieldDefs fds;
        fds.push_back(MkRecord::FieldDef(tstr->value(), ExprPtr(mkarray(tstr->value(), la))));
        return mkrecord(fds, la);
}

I think I have the refine, satisfied and satisfiable logic working with the above type, the problem is with the reification of the value in unqualify. Looking at others, we dispatch based upon the type of some incoming expression. I tried copying that (with no understanding) as

             struct MyUnqualify : public switchExprTyFn {
                    ConstraintPtr constraint;
                    TString* tname;

                    SqlUnqualify(const ConstraintPtr& constraint) : constraint(constraint) {
                            this->tname = is<TString>(constraint->arguments()[0]);
                    }

                    QualTypePtr withTy(const QualTypePtr& qt) const {
                            return removeConstraint(this->constraint, qt);
                    }

                    ExprPtr with(const Var* vn) const {
                            if (vn->value() == "foo") {
                                    ExprPtr r = decodeStrValue(tname);
                                    return r;

                            } else {
                                    return wrapWithTy(vn->type(), new Var(vn->value(), vn->la()));
                            }
                    }
            };

            ExprPtr unqualify(const TEnvPtr&, const ConstraintPtr& cst, const ExprPtr& e, Definitions*) const {
                    return switchOf(e, MyUnqualify(cst));
            }

This however segfaults, trying to compile an Expr with null type. So is the record construction above correct? And if so, how should I go about implementing unqualify?

[kthielen]

Wow you're really getting into the good stuff now! :)

You're right, this part of the pipeline could use a fully worked example with explanation, that would have made your task much less painful (and this is a useful area so well worth reducing the pain here). There are also some unstated assumptions (maybe we could put these explicitly into types).

Since you're so close, maybe I can help try to isolate the problem first?

The assumption made in this unqualify process is that the expressions that come out will be fully type-annotated (they'll have a valid QualTypePtr out of their immediate type() methods and recursively for all child expressions). Since you say that you get a segfault trying to compile an Expr with a null type, my guess is that this assumption has been violated. We could test that idea by commenting out your unqualifier's implementation of with(const Var*) const (this should fail in a different way -- with a complaint about foo being undefined).

Having said that, I'm not sure exactly how you're getting an expression out that doesn't have type annotations (unless maybe your decodeStrValue function is a little different?). The mkarray and mkrecord functions are carefully arranged to produce type-annotated expressions if their inputs are type-annotated.

It might be worth having different Expr types to reflect type annotation (so that it would be impossible to construct an Expr without type annotations where one is expected). That would at least avoid conditions like this. I had that thought a while back but worried that it might produce a lot of boilerplate (having to duplicate or generalize expression functions to cover both forms) but that fear might be unfounded.

[adam-antonik]

Ahh, I see, I'm very sorry, but I took out another entry of the record above. The code above does work, the issue is if I try to make a record with of the form {bar:double} say. I have code to make the type as

            Record::Members ms;
            ms.push_back(Record::Member(str, MonoTypePtr(Prim::make("double"))));
            return Record::make(ms);

And to make the record value

            LexicalAnnotation la;
            MkRecord::FieldDefs fds;
            fds.push_back(MkRecord::FieldDef(str, ExprPtr(new Double(1.0, la))));
            return mkrecord(fds, la);

Is it that my ExprPtr for the double is not not type-annotated? If so, what's the recommended way of doing that?

[kthielen]

Ah ha, that's definitely a problem then. There's an overloaded function constant in lang/expr.H that does this for most primitive types, but (just checked) there's not a case for Double. Arguably the constructor could just set the type anyway, since the type is obviously known in this case. My fault.

Anyway, this should work:

            LexicalAnnotation la;
            auto d = ExprPtr(new Double(1.0,la));
            d->type(qualtype(primty("double")));

            MkRecord::FieldDefs fds;
            fds.push_back(MkRecord::FieldDef(str, d));
            return mkrecord(fds, la);

[adam-antonik]

Thanks, with that and a similar incantation for the general MkArray case I now have nicely typed sql queries working.

[kthielen]

That sounds really interesting. Would you mind elaborating on what you're doing? I'm just curious, I like to find useful unqualifiers especially to show people who think that type classes are the whole story w.r.t. type constraints.

[adam-antonik]

So if we take postgres as an example, we can, given a query string, infer the types and column names of the returned data. Thus, at compile time we can assert that this query will return an array of records of a given type, and at run-time actually perform the query and get data of the required type. So I can say
stuff = exec :: (SQL "select * from table" w) => w
then stuff has type [{column1:type1, ...}]

This I have working, the next step is to allow parameterised queries. Sadly it doesn't seem possible to get the required type of the query from the string, so this will have to be something like
bound :: (SQL a b c) => b -> c
where a is the string and b a type tuple of params to need to be specified, and will be used to call the appropriate param binding function.
So then you could do
ticker_to_exchange = bound :: (SQL "select exchange from stuff where ticker=?" [char] w) => w
and have handy function populated by the table.

[kthielen]

That is a really great idea! Very cool.

For queries with unbound parameters (where you can't infer the type yet), your type signature makes sense. You have a hook in refine to infer c from unique a and b (like the fundep a b -> c), so you don't need users to explicitly write the type of b and c:

chicken = (bound::(SQL "select * from stuff where ticker=?" _ _)=>_)(42)

^---- That would boil down to (SQL "select * from stuff where ticker=?" int x)=>x and then your logic could kick in to determine x

[adam-antonik]

Sorry, but I could use a little advice on my bound param version.
I need the Unqualifier to now return an ExprPtr to a function, as described above, that will based on the constraint, have a given type signature. The simplest way to do this seemed to be to create a new op for for a given TString in the Constraint. If I pass the hobbes context into the Unqualifier's construct and onwards I can do in my with(const Var* vn)

    std::cout << "in bound\n";
    MonoTypePtr typ = c->decodeQueryType(query).first;
    std::cout << "type is " << show(typ) << "\n";
    op * q = new BindQuery(query, c, typ);
    std::string name = ".sql." + str::from(const_cast<::hobbes::SqlP*>(c)->bindQueries++);
    ctx->bindLLFunc(name, q);
    ExprPtr e =  ExprPtr(new Var(name, LexicalAnnotation()));
    std::cout << "bound returning " << show(e) << "\n";

and so, for a given unqualify, create the appropriate op, bind it to a new unique name, and return an ExprPtr of a Var of that new name.
This type-checks, runs correctly when immediately called with a parameter, but produces an odd error of "Failed to get reference to global variable" when the resulting function is assigned. For example:

    > :t (bound :: (SQL "select this from test where that=?" [char] w) => w)
    in bound
    type is [{ this:[char] }]
    bound returning .sql.0
    ([char]) -> [{ this:[char] }]
    > (bound :: (SQL "select this from test where that=?" [char] w) => w)("bar")
    in bound
    type is [{ this:[char] }]
    bound returning .sql.1
    Query returned [{this = ['f', 'o', 'o']::[char]}]
    this
    ----
     foo

    > getThis = (bound :: (SQL "select this from test where that=?" [char] w) => w)
    in bound
    type is [{ this:[char] }]
    bound returning .sql.0
    stdin:1,12-76: Failed to get reference to global variable: getThis
    1 getThis = (bound :: (SQL "select this from test where that=?" [char] w) => w)

(The "Query returned" bit comes from the custom op instance). Any idea as to why this approach doesn't work?

Ah, I see, this doesn't work. If I try
> getThis2 = \x.(bound :: (SQL "select this from test where that=?" [char] w) => w)(x)
in bound
type is [{ this:[char] }]
bound returning .sql.1
Query returned []
So, this thing is getting compiled immediately. I wonder what the right approach to constructing this returned function is

[kthielen]

Interesting, this should be fine so you're not doing anything wrong. One small point is that you can avoid binding low-level functions (which require interfacing with LLVM) and instead add "hidden" definitions through that "Definitions" parameter to unqualify (for example, type class resolution in lib/hobbes/lang/preds/class.C uses this to fill out instances that it generates for specific type sequences on demand).

I can reproduce this independently of your unqualifier this way:

> foo = tupleTail :: (int*double*double)->_
stdin:1,7-41: Failed to get reference to global variable: foo

Looking at it, I think that this is just a silly bug to do with function binding introduced when moving between one of the several breaking API changes made to LLVM and I can put in a fix independent of your work. I guess in the interim (though I should have a fix soon) you can do that eta expansion to work around it:

> foo = \x.(tupleTail :: (int*double*double)->_)(x)
> :t foo
((int * double * double)) -> (double * double)
> foo((1,2.2,3.3))
(2.2, 3.3)

But definitely what you're trying to do is reasonable and should be legal, my fault.

[kthielen]

Turns out this was an issue with global aliases to "LLFuncs" (as with your example and also this tupleTail example), and there is an easy fix for it here: #325

[kthielen]

Sorry to spam you, one more question on your last point -- eta expansion aside, are you concerned with "when" your query runs? That may be a different issue, that you need to delay query execution. You can definitely evaluate queries at "compile time", but depending on what you want to do you might need to divide the query execution so that you can calculate the types at the first stage and then actually run the query for results at the second stage (where results must have the types you decided at the first stage).

If you have questions about how to do that staging I'd be happy to elaborate, but maybe the only issue here was this LLFunc aliasing issue.

[adam-antonik]

Yes, the issue was some confusion about what was where with compile and run-time. Fixed now, thanks very much for the help.