How to properly compare PTSs/languages?

Toxaris / pts

Interpreter for functional pure type systems.

BSD 3-Clause "New" or "Revised" License

21 stars 7 forks source link

How to properly compare PTSs/languages? #121

Closed Blaisorblade closed 10 years ago

Blaisorblade commented 10 years ago

Blaisorblade/pts@3e876fe9911e9a321b2adc22e5f58c5e08dfb481 opens a bug's nest — how do we properly compare PTSs/languages, taking infinite languages into account? The solution I implemented won't work well enough for externally specified languages, but comparing the PTSs themselves won't work easily for infinite PTSs.

We need to choose among nominal or structural equality (named after nominal vs structural subtyping).

Toxaris commented 10 years ago

I feel that language equality should be nominal.

Blaisorblade commented 10 years ago

I feel that language equality should be nominal.

Makes sense. In which case, Blaisorblade/pts@3e876fe9911e9a321b2adc22e5f58c5e08dfb481 is at least correct.

Blaisorblade commented 10 years ago

Closing this for now, I feel the current resolution is sufficient.