So to answer the question directly: No this is not a limitation. You can store an (algebraic) effectful computation in a structure by "thunking" it behind a function that takes unit, like I did above.
February 19, 2025 at 8:48 AM
So to answer the question directly: No this is not a limitation. You can store an (algebraic) effectful computation in a structure by "thunking" it behind a function that takes unit, like I did above.
Languages make this less obvious by putting the effect on the function type, but just think of a monadic computation `m : M a` into a computation `m : () -{M}→ a`. You can always move from the algebraic effects world into the monad world with no issues.
February 19, 2025 at 8:47 AM
Languages make this less obvious by putting the effect on the function type, but just think of a monadic computation `m : M a` into a computation `m : () -{M}→ a`. You can always move from the algebraic effects world into the monad world with no issues.
This may make the connection clearer: Algebraic effects are exactly equivalent to the free monad on some effect signature. Algebraic effects _are_ one specific monad.
February 19, 2025 at 8:46 AM
This may make the connection clearer: Algebraic effects are exactly equivalent to the free monad on some effect signature. Algebraic effects _are_ one specific monad.
This is so beautiful :) thank you for sharing
October 30, 2024 at 7:35 AM
This is so beautiful :) thank you for sharing
I’m more wondering about what desired editing features are shared between languages
e.g in theorem provers there’s a great need for in-depth typing info at every point in the program, but for other languages not so much. Do we target the largest denominator? I’m not sure
e.g in theorem provers there’s a great need for in-depth typing info at every point in the program, but for other languages not so much. Do we target the largest denominator? I’m not sure
December 28, 2023 at 5:19 AM
I’m more wondering about what desired editing features are shared between languages
e.g in theorem provers there’s a great need for in-depth typing info at every point in the program, but for other languages not so much. Do we target the largest denominator? I’m not sure
e.g in theorem provers there’s a great need for in-depth typing info at every point in the program, but for other languages not so much. Do we target the largest denominator? I’m not sure
You look beautiful! Happy Christmas 🙏
December 28, 2023 at 3:59 AM
You look beautiful! Happy Christmas 🙏
Ah man I thought OCaml overloaded record fields 😢 that sucks, good to know
December 26, 2023 at 6:28 PM
Ah man I thought OCaml overloaded record fields 😢 that sucks, good to know
Anyway, to reiterate: Type theory is the study of (notions of) syntactic well-formedness, and what we can derive from it. #proofassistants
December 26, 2023 at 3:57 PM
Anyway, to reiterate: Type theory is the study of (notions of) syntactic well-formedness, and what we can derive from it. #proofassistants
math, or powerful to the point where we can create entirely new logics!
The connection to well-formedness is usually lost in this way - type theory subsumed simpler notions of well-formedness, but it also handles those much more complex cases, and so we focus on them since they’re interesting…
The connection to well-formedness is usually lost in this way - type theory subsumed simpler notions of well-formedness, but it also handles those much more complex cases, and so we focus on them since they’re interesting…
December 26, 2023 at 3:57 PM
math, or powerful to the point where we can create entirely new logics!
The connection to well-formedness is usually lost in this way - type theory subsumed simpler notions of well-formedness, but it also handles those much more complex cases, and so we focus on them since they’re interesting…
The connection to well-formedness is usually lost in this way - type theory subsumed simpler notions of well-formedness, but it also handles those much more complex cases, and so we focus on them since they’re interesting…
There’s an informal well-formedness check in *all* math. Type theory *formalizes* these informal checks!
A type theory is two things: The syntax of the theory, and the typing judgement. This typing judgement can be simple to where it’s reduced to the informal well-formedness left implicit in all…
A type theory is two things: The syntax of the theory, and the typing judgement. This typing judgement can be simple to where it’s reduced to the informal well-formedness left implicit in all…
December 26, 2023 at 3:56 PM
There’s an informal well-formedness check in *all* math. Type theory *formalizes* these informal checks!
A type theory is two things: The syntax of the theory, and the typing judgement. This typing judgement can be simple to where it’s reduced to the informal well-formedness left implicit in all…
A type theory is two things: The syntax of the theory, and the typing judgement. This typing judgement can be simple to where it’s reduced to the informal well-formedness left implicit in all…
“this string of symbols represents an object that I’m working with”. For instance, “nrjfuhejsis” is not a word, and our brains know that automatically! This exact same thing happens in math. For instance I know that “∨×⇔∛∑∪” doesn’t make sense as a logical formula - it’s just a random string! …
December 26, 2023 at 3:44 PM
“this string of symbols represents an object that I’m working with”. For instance, “nrjfuhejsis” is not a word, and our brains know that automatically! This exact same thing happens in math. For instance I know that “∨×⇔∛∑∪” doesn’t make sense as a logical formula - it’s just a random string! …
like guaranteeing the absence of unsafe casts, like interpreting a string as an integer or what have you
The mathematical context for this is interesting. In any sort of math, we have the syntax for what we’re doing - the notation we use to represent our objects - and we have some notion of…
The mathematical context for this is interesting. In any sort of math, we have the syntax for what we’re doing - the notation we use to represent our objects - and we have some notion of…
December 26, 2023 at 3:40 PM
like guaranteeing the absence of unsafe casts, like interpreting a string as an integer or what have you
The mathematical context for this is interesting. In any sort of math, we have the syntax for what we’re doing - the notation we use to represent our objects - and we have some notion of…
The mathematical context for this is interesting. In any sort of math, we have the syntax for what we’re doing - the notation we use to represent our objects - and we have some notion of…
Please show me! I haven’t yet run into the situation you describe
December 26, 2023 at 2:52 PM
Please show me! I haven’t yet run into the situation you describe
trying out new features and axioms in their type theories, seeing whether those additions make sense and what semantics they can be given. Type theory is much more broad and diverse than set theory. Perhaps this will change as it ages and we will settle on a single theory like people settled on ZFC.
December 25, 2023 at 9:34 PM
trying out new features and axioms in their type theories, seeing whether those additions make sense and what semantics they can be given. Type theory is much more broad and diverse than set theory. Perhaps this will change as it ages and we will settle on a single theory like people settled on ZFC.
For instance homotopy type theory interprets types not as sets but as *topological spaces*, giving rise to a new and useful axiom (called "univalence").
Type theory is very different from set theory in its diversity - set theorists have mainly settled on ZFC, whereas type theories are constantly...
Type theory is very different from set theory in its diversity - set theorists have mainly settled on ZFC, whereas type theories are constantly...
December 25, 2023 at 9:32 PM
For instance homotopy type theory interprets types not as sets but as *topological spaces*, giving rise to a new and useful axiom (called "univalence").
Type theory is very different from set theory in its diversity - set theorists have mainly settled on ZFC, whereas type theories are constantly...
Type theory is very different from set theory in its diversity - set theorists have mainly settled on ZFC, whereas type theories are constantly...
and we trust sets, so we believe we can trust types. Type theory is the syntax, set theory is the semantics.
The neat thing is that set theory isn't the only semantics we can give to type theory! I've been saying "type theory" as if it's all one thing, but there are *many* different type theories…
The neat thing is that set theory isn't the only semantics we can give to type theory! I've been saying "type theory" as if it's all one thing, but there are *many* different type theories…
December 25, 2023 at 9:31 PM
and we trust sets, so we believe we can trust types. Type theory is the syntax, set theory is the semantics.
The neat thing is that set theory isn't the only semantics we can give to type theory! I've been saying "type theory" as if it's all one thing, but there are *many* different type theories…
The neat thing is that set theory isn't the only semantics we can give to type theory! I've been saying "type theory" as if it's all one thing, but there are *many* different type theories…
This is exactly the relationship between type theory and set theory. Set theory is old and trusted, while type theory is new and quickly evolving. We thus make sure all our new type theories are logically consistent by *interpreting* them into set theory - we can think of types in terms of sets...
December 25, 2023 at 9:29 PM
This is exactly the relationship between type theory and set theory. Set theory is old and trusted, while type theory is new and quickly evolving. We thus make sure all our new type theories are logically consistent by *interpreting* them into set theory - we can think of types in terms of sets...
This happens all the time in math! How do we know we can trust new methods of reasoning (new logics)? The best way is essentially just to related it to some older method of reasoning (older logics) that we already trust. The new logic is called the "syntax" and the old logic is the "semantics"...
December 25, 2023 at 9:24 PM
This happens all the time in math! How do we know we can trust new methods of reasoning (new logics)? The best way is essentially just to related it to some older method of reasoning (older logics) that we already trust. The new logic is called the "syntax" and the old logic is the "semantics"...
translate the formulas from this untrusted logic to the trusted one. Maybe you try some other, more indirect translation. But either way, what you're trying to do is *define* the untrusted logic in terms of the trusted one
What you've stumbled on is the distinction between "syntax" and "semantics"…
What you've stumbled on is the distinction between "syntax" and "semantics"…
December 25, 2023 at 9:20 PM
translate the formulas from this untrusted logic to the trusted one. Maybe you try some other, more indirect translation. But either way, what you're trying to do is *define* the untrusted logic in terms of the trusted one
What you've stumbled on is the distinction between "syntax" and "semantics"…
What you've stumbled on is the distinction between "syntax" and "semantics"…