This works well with Unix command line interpretation, as the success value is 0 for no tests failed. If even one test fails, the output code of the program will be interpreted as failure by standard Unix tools.

Hello,

It's the first time I hear about glossopoeia/boba and it wasn't nice at all. I never starred, forked and/or participated in any other way in this repo. Nevertheless, I've got a spam email with the following content:

I hope it wasn't intentional.

There is currently a semantic issue when a handle expressions that calls a handler, then resumes, then tries to reference a variable from a scope outside the handle expression.

Example of something that shouldn't work right now:

let x = 1;
handle {
    hdlr! x
} with {
    hdlr! => ;
}

So something like

Empty a, Semigroup a ==> Monoid a

Helps reduce the number of constraints in printed types, and also allows for writing simpler types.

Currently propagation rules are added to the type environment as they are encountered in the source code during compilation. This means that 'orphan' rules may not be available during type inference if a function that relies on the overloads is defined prior to the 'orphan' rule.

This problem is already solved for instances (and 'orphan' instances), so we should be able to use a similar method to gather rules, with the caveat that rules are not specific to a particular overload: a rule should only be added to the type environment if all of the constraints in the head and result components are defined. The last-defined overload will be the one that includes all rules that mention it.

Right now it correctly outputs which tests have failed, but it is hard for a developer to determine what the failure is.

Currently only one is supported due to compilation trickiness, would like to resolve this and support more than one.

Since iterator for loops are compiled down to handlers maybe there is a straightforward way to do this with injection.

Or maybe a dotted effect? That would be interesting, semantics could probably handle it but the type system might not.

Worst case scenario it can be done with a few definitions for multiple argument iterators, i.e. yield1!, yield2!, etc.

Currently it finds all re-exported names (recursive for all imported units as well) and then filters to just the explicitly re-exported names.

Instead, it should look at the explicitly re-exported names, and find the base declaring unit of the name. Still recursive but no longer builds a (potentially big) tree only throw most of it away.

Currently, the programmer has to specify the sharing and validity constraints manually in constructor types for the compiler to get them right. For instance, instead of writing

rec data List a
    = Cons (List a) a --> (List a)
    | Nil --> (List a)

the programmer has to write

rec data List x
    = Cons {(List {a vd sd}) (vd & vl) (sd | sl)} {a v s} --> {(List {a (vd & v) (sl | s)}) (vd & v & vl & vr) (sd | sl | s | sr)}
    | Nil --> {(List {a v s}) (v & vr) (s | sr)}

Writing out the latter is tedious and easy to get wrong. But it's very pattern based and seems like it should be easy to automatically generate.

The concerns with automating this are:

1. Will it be polymorphic enough?
2. Will it be too polymorphic?
3. Can the programmer plug in some custom sharing attributes without breaking it?

Formats:

• Octal
• Binary
• Hex

All primitive numeric types and size of types should be supported.

Ideally enforcing:

• Termination
• Confluence

This is a particular problem with multishot effect handlers, which may require more lets than necessary to compose nicely.

For instance, in the amb! tests in the examples folder, the handler:

flip! => False resume True resume append-list

must currently be written as:

flip! => {
            let x = False resume;
            let y = True resume;
            x y append-list
        }

due to the semantics not having enough information to determine how many values should be passed back to the continuation stack.

We can use the type declaration of the effect to determine how many values should be passed back.

Causes runtime panics due to malformed core-generated code semantics when there's more than one output generator. Second generated value is too far down the stack and causes the first to be overwritten

Problem is found in the typeable test file.

Core issue is that a perfectly valid instance definition can infer a type that is actually more general than the overload. In this case we can let it pass, but we need to be careful that the instance actually consumes and produces the expected number of elements from the stack still. If it does not consume and produce enough, any function which uses that instance will be unsoundly typed.

Try to run test on test/tuples.boba. Type inference will pass but runtime will crash due to calling the wrong equality overload param during a tuple equality check.

Currently ambiguity checking is a no-op, which means that the compiler will try to generate code for ambiguous functions. Seems like it fails to do so in a lot of cases, which is good, but it also fails with unclear error messages or guidance toward resolving the problem.

Implement an explicit ambiguity check that at least points to the function that has the type problem.

Just unimplemented right now, but very important to resolve for general purpose programming use cases. Will also allow to remove some cruft from the code generator.

Right now it is possible to 'leak' effects out of the type system by hiding effectful calls in overloaded function instances. It is up to the overload designer to predict what effects will be needed and define them in the overloaded function type signature, which is obviously asking for big trouble.

There's two options here:

Option 1: Ban non-declared effects from escaping an instance.

Basically akin to throwing up our hands and waving the white flag. Tempting from a compiler developer perspective, but I just know this will eventually cause complaints about usability. It is, however, easy to make sound and straightforward to think about for the average developer: just 'handle' any effects that need to be handled, and wrap them in a result type if you really want them to escape.

Option 2: Join all inferred effects, permissions, and totality attributes inferred on instances into the overload effect/permission/totality.

We should remove effect, permission, and totality attributes from appearing in the overload function definition at all. Only input and output sequences will be allowed, and only those will affect instance overlap checking and inferred type matching.

During instance gathering, the inferred effect, permission, and totality of each instance will be unified together into one large effect type for overall overload method signature.

So something like:

test multiple-out? = 1 2 is 3 2 should type check, but partially fail at runtime with 1 != 3.

This should be straightforward to implement with the gather method as a simple pre-type-checking code transformation in the test code generator.

Type inference for functions that have multiple functional dependency constraints can cause the compiler to hang in the CHR implementation. I don't believe it is looping, but it is ineffeciently computing all possible reductions. The reason the compiler pursues all possible reduction paths, instead of choosing one, is to verify that the rule set is confluent, since we have no way to do that before the rule set is run currently.

Standard repository request. The most key type system tests are run via dotnet test right now, so just need to hook into that.

It's convenient enough to miss it a lot of times and makes many simple string literals more readable. But it would be nice if this was just a syntactic sugar of some sort, driven by an overload or something.

So, $"Hello there, {name}, and welcome!" would be desugared into "Hello there, " name show concat-string ", and welcome!" concat-string.

Will make use of the fixed-size Abelian type defined in Boba.Core

1. Iterable in for loops
2. Special syntax for creating with compile-time known size
3. Primitive functions for accessing/setting elements while maintaining uniqueness