René's URL Explorer Experiment

Title: Row/class/interface existential quantifier · Issue #34 · rowscript/rowscript · GitHub

Open Graph Title: Row/class/interface existential quantifier · Issue #34 · rowscript/rowscript

X Title: Row/class/interface existential quantifier · Issue #34 · rowscript/rowscript

Description: This feature is not necessarily needed in the first-ever major release of the language. Why do we need them though? It's actually like Agda's records, just a furnished Sigma type that can contain some type information out of some functio...

Open Graph Description: This feature is not necessarily needed in the first-ever major release of the language. Why do we need them though? It's actually like Agda's records, just a furnished Sigma type that can contain s...

X Description: This feature is not necessarily needed in the first-ever major release of the language. Why do we need them though? It's actually like Agda's records, just a furnished Sigma type that can c...

Opengraph URL: https://github.com/rowscript/rowscript/issues/34

X: @github

direct link

Domain: github.com

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Row/class/interface existential quantifier","articleBody":"This feature is not necessarily needed in the first-ever major release of the language.\r\n\r\n* Why do we need them though?\r\n\r\nIt's actually like Agda's records, just a furnished Sigma type that can contain some type information out of some functions, so you could say it's just **existential types**. For example:\r\n\r\n```ts\r\nfunction foo\u003cT>(data: T): Bar {\r\n    return Bar{type: T, data: data}\r\n}\r\n```\r\n\r\n* Ouch, the name is so bad...\r\n\r\nYes, we definitely need a good name for this construct. It could be **dependent records** for now.","author":{"url":"https://github.com/anqur","@type":"Person","name":"anqur"},"datePublished":"2023-04-01T04:43:57Z","url":"https://github.com/rowscript/rowscript/issues/34"}

Links:

Viewport: width=device-width