effekt-lang
Machine: Handle evidence
Handle evidence and use it to execute effect operations in the correct context.
Is not yet correctly implemented in the llvm backend (number of stacks to pop is ignored), so widely untested.
For some reason, fibonacci.effekt works on my machine but fails in the CI.
Also, while I wanted to use infixAdd for my first draft, resolving that Symbol in the Context sometimes failed, so I added EviAdd.
For some reason, fibonacci.effekt works on my machine but fails in the CI.
Maybe stack size?
If we absolutely have to add EviAdd then I would call it something like ComposeEvidence.
If we absolutely have to add
EviAddthen I would call it something likeComposeEvidence.
Ah, yes, that's a better name.
https://github.com/effekt-lang/effekt/pull/164/commits/f85fb62a1d8a3d6657680bffab0cc3a98248403a uses "infixAdd" instead of ComposeEvidence. I'm not sure if that is preferable?
Note: the current implementation would break if the type of infixAdd changed from (Int, Int): Int.
@phischu tested it on his machine and it was indeed the stack limit being reached.
I have now semi-splitted out evidence. It is still synonymous int in most places (i.e. machine.builtins.Evidence is machine.Type.Evidence etc), but can be used as if it weren't (there is a type alias Evidence, and builtins.Here (=0) and builtins.There(_) (=_+1) work for both construction and patterns).
Why does There take another evidence? It should just alias the number 1 IIUC.
I think both are reasonable. I understand Here and There as the constructors of the evidence type, so There just says "outside of the current region" and still needs specification/proof as to where exactly (like with e.g. Data.List.Relation.Unary.Any etc in Agda).
I am not strongly opposed to changing it to There : Evidence = 1, although I think it's nicer this way, as it allows to construct all possible evidence values without using + (on Int).