nprofile1q…4rrqe nprofile1q…eyqfl nprofile1q…ndand My beef with the lambda cube ...

Why Nostr? What is Njump? Join Nostr

npub1cj…fxs07

2025-10-15 18:10:42 UTC

in reply to nevent1q…t80q

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyr2n36a7k44xnepjzejv2c77yrnxdxp5n025wgnd4884ncm8ep8wqaeyqfl (nprofile…yqfl) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp2aucj8nm0d5n2ls2z3dy2z5udpsplzpjq60kur0q9qfax33370cyndand (nprofile…dand) My beef with the lambda cube (not sure if this is a similar beef) is that it puts an overly strong emphasis on being able to quantify over various things in *closed terms*, and thus misses that *judgments* (terms in a context) are the central object of study in type theory, and additionally the right model for the top-level bindings in a language. E.g. you can have top-level functions without having function types, and you can have top-level generic functions without having forall types. It took me a while to realize this.

Author Public Key

npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07

Seen on

wss://relay.ditto.pub

Show more details

Published at

2025-10-15 18:10:42 UTC

Kind type

1 Short Text Note

Event JSON

{ "id": "bc837118dfb5137ed7c50c91f9abc1e4bb3fa4cb61fa71b9620e818b96693f2c", "pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a", "created_at": 1760551842, "kind": 1, "tags": [ [ "p", "934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49", "wss://relay.ditto.pub/" ], [ "p", "d538ebbeb56a69e4321664c563de20e66698349bd547226da9cf59e367c84ee0", "wss://relay.ditto.pub/" ], [ "p", "55de62479ededa4d5f8285169142a71a1807e20c81a7db83780a04f4d18c7cfc", "wss://relay.ditto.pub/" ], [ "p", "a859a34b101281dd2f0bcb9f1ac28e84a8151b97d5007d033a40728ec3f05e34", "wss://relay.ditto.pub/" ], [ "p", "eb1cda06a29fa6db324928163835bdc74cfc337c90c9c5027f3637a9eff3071c", "wss://relay.ditto.pub/" ], [ "p", "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301", "wss://relay.ditto.pub/" ], [ "e", "57bec0de6b71987bf9a421cbb4306a8dc64c9f752bc080e88ac2376f507c99d2", "wss://relay.ditto.pub/", "reply" ], [ "proxy", "https://mathstodon.xyz/users/olynch/statuses/115379525545476973", "activitypub" ], [ "client", "Mostr", "31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr", "wss://relay.ditto.pub/" ] ], "content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyr2n36a7k44xnepjzejv2c77yrnxdxp5n025wgnd4884ncm8ep8wqaeyqfl nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp2aucj8nm0d5n2ls2z3dy2z5udpsplzpjq60kur0q9qfax33370cyndand My beef with the lambda cube (not sure if this is a similar beef) is that it puts an overly strong emphasis on being able to quantify over various things in *closed terms*, and thus misses that *judgments* (terms in a context) are the central object of study in type theory, and additionally the right model for the top-level bindings in a language. E.g. you can have top-level functions without having function types, and you can have top-level generic functions without having forall types. It took me a while to realize this.", "sig": "e166244b35de5753530eab42c0d714af46dbf9b03880b0e4308636110f2cee8d6aa709fe97cc2d224af69741ff226e46f50a534282c21d7ef95d9a71ac283205" }