How functional is this?

[atennapel]

Is this implementation complete? If not, are you aware of any other implementations?

[mrkgnao]

No, it is not finished, and I am not aware of any others.

That said, it is almost complete, if I remember correctly, and I do plan to return to it and fill in what's missing; the "structure" of the typechecker is complete. Strictly speaking, what is implemented is essentially (likely an unsound and incomplete) subset of Sound and Complete: most of the remaining work amounts to implementing the rest of the judgments/rules. All the functions in Infer.hs have a list of the rules corresponding to them as comments, with the unimplemented ones identifiable as having no code following the name of the rule. To the best of my memory, most of the remaining work is in implementing the coverage checker here:
https://github.com/mrkgnao/sound-and-complete/blob/master/src/Infer.hs#L1492

There are a few examples of expressions that can be typechecked, etc. here:
https://github.com/mrkgnao/sound-and-complete/blob/master/src/Tests.hs#L62

[fluffynukeit]

As of October 2019 (now), is your description of the work yet to be done still accurate? Presuming so due to lack of commits since this thread started.

[atennapel]

I don't think anything changed in this repo, and I also haven't been able to find any complete implementation anywhere else.

[fluffynukeit]

FYI the type system rules in the published 2019 version are sometimes different compared to the 2016 draft that was used for this implementation.

2016 draft
2019 published

The differences I noticed were primarily how principality is handled in some cases, as well as labels used for different rules. I discovered this while studying the implementation, trying to correlate the code to the 2019 paper and coming up short until I compared it to the 2016 draft, when some choices/labels started making more sense.

This late 2018 version looks quite similar to the POPL 2019 one but includes appendices.

[mrkgnao]

@fluffynukeit correct, I haven't had time to work on this since unfortunately

[fluffynukeit]

I wrote my own implementation here: https://github.com/fluffynukeit/scbt

I believe it is complete, but I do need to add more test cases for finding implementation bugs (got one already) because the only implemented tests right now are lifted straight from the small example in the paper. It also needs a lot more user-friendliness polish. But generally I think all the rules are present.

[atennapel]

That's awesome!