I'm implementing a type theory where the top-level bindings are *judgments* in the theory, rather than closed forms (this is important because I only have a restricted pi type). This means that evaluating an identifier (in the context of nbe) doesn't necessarily produce a "value" in the traditional sense. So I have two options:
1. Have eval return a sum type of (closed value, judgment)
2. Extend my type of values to include these "non-values".
Has anyone else run into this kind of problem before? Do people have recommendations for solutions?
Owen Lynch
npub1cj…fxs07
2025-12-28 20:27:35 UTC
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-12-28 20:27:35 UTCEvent JSON
{
"id": "232ce2e994d8f6e78929437442d6bc3b1b813305c376d84d3a2c9b42cfd0858b",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1766953655,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115799074737706196",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "I'm implementing a type theory where the top-level bindings are *judgments* in the theory, rather than closed forms (this is important because I only have a restricted pi type). This means that evaluating an identifier (in the context of nbe) doesn't necessarily produce a \"value\" in the traditional sense. So I have two options:\n\n1. Have eval return a sum type of (closed value, judgment)\n2. Extend my type of values to include these \"non-values\".\n\nHas anyone else run into this kind of problem before? Do people have recommendations for solutions?",
"sig": "41fd0fb0242ce39d0adad0afbd1915e8e1a2fafe6b82287eef79fb865c06fb2e423bcd90540ef23d1627aa612a8d4a5e4b5bb4b90a0dbe15b1b5a512895f7fed"
}