catnaroek

16 ms·

91.
by catnaroek 9y ago
> Strong typing simply means that every value in the language has one and only one type, whereas weak typing means that some values can have multiple types. Aha! Now, any system with subtyping is “weakly typed”! For example, System F-sub
92.
by catnaroek 9y ago
> You then provided an example of something you claimed could not be done monadically. Using a monad , i.e., an endofunctor with unit and join that satisfies the well-known laws, you cannot do it. > I pointed out that you could imple
93.
by catnaroek 9y ago
> Monads have nothing to do with verification, so I'm now unsure what your original point was. Indeed, monads are about language semantics, prior to any verification attempt. Have you tried actually tried reading my original comment
94.
by catnaroek 9y ago
Of course, you don't need types to write programs. Types are just a way to mechanically verify some desirable properties. But, as it turns out, resource management in large programs is pretty damned hard to get right without this kind
95.
by catnaroek 9y ago
No, you need proper substructural types. Not even monadic regions will help.
96.
by catnaroek 9y ago
> In this post we’ll have a look at some instances of such sitations, their “ad hoc” solutions provided at the language level, and finally at how these problems can be solved in a uniform way using Monads. I wonder if the blog post'
97.
by catnaroek 9y ago
How do you measure simplicity?
98.
by catnaroek 9y ago
It is for purely pragmatic reasons. Try actually writing calculational proofs using long identifiers. You will soon find yourself wanting to be drowned in lava. Of course, a true programmer delegates even the simplest calculation to a com
99.
by catnaroek 9y ago
> Seems like maybe this is all just a clash between formalism and how languages work in practice, I think you missed the word “broken”, before “languages”. Sums in Standard ML are really sums. > similar to how it's nice to just p
100.
by catnaroek 9y ago
The universal property for a sum type that having an X-valued function from a sum is equivalent to having X-valued functions from each summand, for any type X. In other words: (0) There exists a procedure “foo” that recovers the functions f
101.
by catnaroek 9y ago
> My understanding is that "tagged unions" and "sum types" are the same thing Well, your understanding is wrong. Sum types satisfy a specific universal property, which union types don't.
102.
by catnaroek 9y ago
It is good at neither. Union types and sum types are veeery different from each other.
103.
by catnaroek 9y ago
> abstract types can break merely by having a stronger type system which is able to prove strictly more things (such as whether two types are equal) Indeed, which is why I'm not such a huge fan of overly powerful type systems. >
104.
by catnaroek 9y ago
No idea about you, but when I reason about programs, I spend very little time manipulating syntax. Most of the time is spent manipulating semantic objects, like predicates on the program state, whose representation is independent from eve
105.
by catnaroek 9y ago
Union and intersection types make the following assumptions: (0) There is a single physical universe that contains all values. (1) The role of types is to “carve out” fragments of this universe. (2) Say you have two values `x` and `y` of
106.
by catnaroek 9y ago
What you propose breaks completely as soon as you want to define and use abstract types.
107.
by catnaroek 9y ago
It is relevant, because it means that while `|` may produce a disjoint union if its arguments are already disjoint, it is not guaranteed to produce a disjoint union in the general case. Hence, my original comment had a point. As if that
108.
by catnaroek 9y ago
But then it isn't disjoint.
109.
by catnaroek 9y ago
A union type `A | B` in Flow is disjoint if and only if the types `A` and `B` are a prior known to be disjoint. There is no equipping `A` and `B` with fresh new tags to force them to be disjoint.
110.
by catnaroek 9y ago
Um, re-read the documentation: > These disjoint unions are made up of any number of object types which are each tagged by a single property . It is clearly a disjoint union in the set-theoretical, not category-theoretical sense. Let&#x2
111.
by catnaroek 9y ago
Confusingly, there are two different things called disjoint union in mathematics. One is what you mentioned, which is indeed the coproduct in the category of sets. But another one is simply the union of two disjoint sets, which might not be
112.
by catnaroek 9y ago
Sum types are a universal construction: you take any two types, and produce yet another type. In particular, you can sum a type with itself. Disjoint unions give you nothing of the sort. In other words: learn to mathematics.
113.
by catnaroek 9y ago
No, they haven't. Union types and sum types are semantically very different from each other.
114.
by catnaroek 9y ago
> I was offering what I suspect the parent post meant by it being easier to reason using the mechanics of the language. And it still doesn't make sense. “Reasoning about programs” is making inferences about their meaning , i.e., de
115.
by catnaroek 9y ago
> To that end, how things are actually implemented takes a trip to assembly. Don't confuse “defined” with “implemented”. This is the entire point to having an axiomatic semantics! > My point was that you don't typically see
116.
by catnaroek 9y ago
> In lisp, everything's can be expressed in terms of other lisp code. Um, and how exactly are primitive forms defined? > most keywords get the explanation of "this is how the computer will act" and then explanations of
117.
by catnaroek 9y ago
> very easy to reason [sic] about by built-in mechanisms in that language. Languages allow you to express your reasoning, but they don't do the reasoning by themselves. Also, there is no conclusive evidence that homoiconic langu
118.
by catnaroek 9y ago
It would actually be more interesting if someone made a list of useful systems that cannot perform general computation. Some examples: (0) Parsers for context-free grammars (1) Relational algebra, and the subset of SQL that maps to it (2)
119.
by catnaroek 9y ago
Mathematicians look for more elegant proofs of already proven theorems all the time. The earliest proof is usually not the simplest, nor the clearest, nor the easiest to generalize, nor <insert desideratum here>. Similarly, I think th
120.
by catnaroek 9y ago
> I have heard, for instance, that's it's actually very difficult in rust to write a linked list without dropping to unsafe code. It is also hard in C to write a linked list without dropping to unsafe code. In fact, it is hard

More ›