search

anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Missing type/object for left and right morphisms #53

Closed jonaprieto closed 1 year ago

jonaprieto commented 1 year ago

Please consider adding the Object information missing from the left and right morphisms. Say left a is of object coprod A B, I expect to write in the future left a B, as the object for a can be inferred. We plan to use this info to have a simple type-checking/inference algorithm for the Geb backend of Juvix.

lukaszcz commented 1 year ago

It's about your stlc datastructure (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp). If you don't have the type info about missing option in left/right coproduct injection, then not every term has a unique type. That's also the case when you don't have the result type specified in the absurd constructor (which you don't), so also consider adding that one.

rokopt commented 1 year ago

Agreed, we'll add these.

rokopt commented 1 year ago

70 includes code to address this (including for absurd as well as left and right).

rokopt commented 1 year ago

Done in #81 .