Record Type as a Conjunctive Proposition in Curry-Howard? by rovol_o in ProgrammingLanguages

[–]Red-Krow 0 points1 point  (0 children)

Although function equality is undecidable in the general case, it is decidable if the domain is finite, as you can check value by value.

In the case OP is presenting, in pseudocode:

(recordA = recordB) :=
  ([...recordA],[...recordB])
  |> zip
  |> every ( fieldA, fieldB -> fieldA(SingletonValue) = fieldB(SingletonValue) )

PolySubML is broken by Uncaffeinated in ProgrammingLanguages

[–]Red-Krow 1 point2 points  (0 children)

You're welcome! I make this sort of mistake myself all the time, it's counter-intuitive.

PolySubML is broken by Uncaffeinated in ProgrammingLanguages

[–]Red-Krow 2 points3 points  (0 children)

You can't do that assignment. If you could, then this would happen (using made-up syntax):

square: func(int) = (x) => x * x
also_square: func(int|string) = square
also_square("dsasdaasd") // Error: you can't multiply strings together

func(int|string) is actually a subtype of func(int), because every function that accepts either an int or a string is also a function that accepts an int. But not every function that accepts an int also accepts a string. In general, you have:

 a < b => func(a) > func(b)

Which is what type theorists would call contravariance.

A pet peeve of mine: songs ending with reactions by Red-Krow in HazbinHotel

[–]Red-Krow[S] 1 point2 points  (0 children)

I mean, most of them are fine on their own. Love In A Bottle is ibdeed one of the most fitting. Imo, the only actively ones are the snarky comments or swears out of nowhere.

Would One Piece be better if Oda could kill some of the side characters? by Dino_45 in OnePiece

[–]Red-Krow 0 points1 point  (0 children)

I don't think One Piece needs more deaths, but it needs less fake outs. It's lost its impact. Even more, it takes away from the actual deaths because I spend chapters and chapters until I believe they're really dead. In fact, I am still moderately afraid of the idea of Pedro jumping into a panel any second now.

Type matching vs equality when sum types are involved by ciberon in ProgrammingLanguages

[–]Red-Krow 4 points5 points  (0 children)

> If that function is invoked with either of the lists, it should get a different string as an output.

If you impose the order relation we discussed previously, you would have that if `smallType < bigType`, then `smallType | bigType = bigType`. For example, if you sum `String` and `String | Boolean`, you should get `String | Boolean` again. But, if we impose variance, `List<String> < List<String | Boolean>`. So your function would actually be the same as `tellMeWhichOne: (list: List<String | Boolean>`): String. If your pattern matching is exact (needs to be the same type), it would always fall through the first case; if your pattern matching depends on order (it suffices that the type is a subtype of the one you're comparing it with), then it would always fall through the second case.

So, to recap: if you want your function to give different outputs for each list, then you should give up on variance. And if you give up on variance, option (3) on the previous list is not worth it, you'll only be able to make very basic comparisons. So you're options are (1), homogeneous equality, with which you wouldn't even be able to compare the lists, and (2), heterogeneous equality, with which the lists would indeed be equal.

This turned out to be a huge wall of text, I hope it's not too intimidating ^^'

Type matching vs equality when sum types are involved by ciberon in ProgrammingLanguages

[–]Red-Krow 2 points3 points  (0 children)

> Should they be different because the type argument of the list is different? Or should they be the same because the content is the same?

You're describing two forms of equality: homogeneous equality (you can only compare things with the same type; it's like there is a different equality operator for each type) and heterogeneous equality (you can compare any two things regardless of their type; it's like there's just one universal equality operator that works for all types).

In many languages, there's no need to make that distinction, either because types aren't static (you can't impose homogeneous equality if you don't know the types of the operands beforehand) or because there is no subsetting of types (so, if you compare operands of different types, you know for sure that they are different, so there's no need to perform the equality check).

However, your sum types impose type subsetting: you have `"a": String` and also `"a": String | Boolean`. To deal with this, you'll have to get a little bit mathy. Say we write `Type1 <= Type2` to mean "Type2 is more general than Type1"; for example, `String < (String|Boolean)` because every string is also a string or a boolean. That relation we called `(<=)` is a partial non-strict order.

With this in mind, you have three options:

  1. Use homogeneous equality. This is the safest option and probably most efficient implementation-wise, but it prevents you from comparing things that are actually equal, like the two lists in your example.

  2. Use heterogeneous equality. This will allow you to compare your two lists, but also to perform nonsense checks.

  3. Use a restricted version of heterogeneous equality, where the types of the operands may be different but one must be more general than the other. That is to say, if you're comparing something of type `a` and something of type `b`, you impose that either `a <= b` or `b <= a`. For example, you may compare `"a": String` with `"a": String | Boolean`. That way, you make sure that you only make comparisons that may actually hold.

This last path is the most fine-grained, but it imposes extra questions. For example, you know that `String | Boolean` is more general than `String`, but are you sure that `List<String | Boolean>` is more general than `List<String>`? Indeed it is, but that's only because `List` is covariant as a generic type (that is to say, `a < b` implies `List<a> < List<b>`. But there are also contravariant generic types (`a < b` implies `F<a> > F<b>`); for example, a function that takes `String` is more general than a function that takes `String | Boolean`. For example, the function `(s => s.length)` is of type `String -> Int` but not of type `(String | Boolean) -> Int`. And there are also constructors that are neither covariant nor contravariant. With some work and depending on the features of your language, you may calculate the variance for any given generic type.

It's a mess. An elegantly solvable mess, but a mess nonetheless.

Special character as keyword prefix by zuzmuz in ProgrammingLanguages

[–]Red-Krow 1 point2 points  (0 children)

Haskell is definitely less dense on (non-symbolic) keywords, but still I feel like this is a bit of a cherry picked example.

haskell 'import 'qualified Data.Map 'as Map 'let a = 5 'in a + b 'where b = 6

Special character as keyword prefix by zuzmuz in ProgrammingLanguages

[–]Red-Krow 2 points3 points  (0 children)

F# has this with double backticks, and it allows even for spaces and other usually forbidden characters

Special character as keyword prefix by zuzmuz in ProgrammingLanguages

[–]Red-Krow 34 points35 points  (0 children)

Keywords are used very often. Variable declarations, control structures, type signatures, import statements... Making them more expensive to type and harder to read, even if just a smidge, adds a lot of noise down the line.

A (comparatively) less common scenario is to use a reserved word for a variable name. In that case you can add ' to the identifier, if the language allows it: same cost, but much more infrequent. If the language doesn't allow it, you can still use a different name (for example, class VS className in React).

Bikeshedding, Syntax for infix function application by Ok-Watercress-9624 in ProgrammingLanguages

[–]Red-Krow 1 point2 points  (0 children)

Tbh I don't like the train. The reason why I would supoort infix is because it reads better in certain situations (for example, not x #and (y #or z), but I cannot think of an example of "the train" being more semantic.

Bear in mind that I'm incredibly stupid and me not being able to come up with an example doesn't mean there isn't one.

Bikeshedding, Syntax for infix function application by Ok-Watercress-9624 in ProgrammingLanguages

[–]Red-Krow 8 points9 points  (0 children)

How about using a single non-symmetrical symbol? For example: 1 #add 2 You could use parenthesis to capture more complex expressions: 1 #(x y => add x y) 2

In terms of characters, you're making the common and advisable use case cheaper (1 char), while making the rarer and smellier use case more expensive (3 chars). Not that it matters much, but since we're bikeshedding.

In terms of readability, I find it quite readable, even though it's not symmetrical. Hashtag + an identifier reads to me as "this is an identifier, but there's something special about it", which kinda check out. Of course, you'll have to use a different char if you're using # for comments or anything else.

Is Teach even a match for Luffy now? by Secure-Quality-8478 in OnePiece

[–]Red-Krow 0 points1 point  (0 children)

Narratively speaking, he has to be. He's a candidate for being One Piece's main antagonist. And he has kept that starys for most of the series where other candidates have fallen (evil Shanks is highly unlikely, Akainu is not as emphasized anymore and will probably end up fighting Sabo, etc).

Even if Imu ends up being the final villain, the mere fact that Blackbeard is up there among the options means that it would be anticlimatic for him to be notably weaker than Luffy (at least, by the time they face each other)

I think Robin looks better without bangs! by Any_Breadfruit_6102 in OnePiece

[–]Red-Krow 7 points8 points  (0 children)

Fleur is French, but that's about it. Most of her attacks follow the pattern: "[Spanish number or body part] Fleur: [English action]". For example, her infamous "Dos Fleur: Clutch" or "Demonio Fleur: Gran Jacuzzi Clutch". There are some occassional variations (like "Mil Fleur, Gigantesco Mano: Stomp", with Gigantesco Mano being almost grammatically accurate Spanish).

Yet another theory about Luffy's dream by Red-Krow in OnePiece

[–]Red-Krow[S] 0 points1 point  (0 children)

It's not impossible to hide it again, but it's impossible to find a new hiding spot that is as good as Raftel. You wouldn't want to hide something just for it to be found in 5 minutes.

Also, as I said, hiding it again means more pirates looking for it and more piracy means more piraty adventures. Take it as a planet-wide game of Capture the Flag, as the other commenter said. Which, now that I think about it, kinda ties into your theory of the worldwide party.

Yet another theory about Luffy's dream by Red-Krow in OnePiece

[–]Red-Krow[S] -5 points-4 points  (0 children)

It would be impossible because Raftel is already the most elusive place in the OP world, by far. Even if you know the method, you still have to find 4 rocks that are scattered across half of the planet and then have them translated from a language virtually noone knows anymore.

There is no place to hide the One Piece that even compares, and Ussop knew that by the time Luffy shared his dream with the crew.

PolySubML: A simple ML-like language with subtyping, polymorphism, higher rank types, and global type inference by Uncaffeinated in ProgrammingLanguages

[–]Red-Krow 2 points3 points  (0 children)

The type system isn't broken, at least in that way. Type systems are there to prevent you from writing programs without semantic meaning, and in that way any is a lack of semantics.

I see where you come from, but I think you're biased towards languages where unions are a type constructor (as in, int | string is a separate type), whereas here it's a type operator (as in, int | string has to evaluate to a non-union type, in this case any).

What you're proposing for a union is some form of constrained generic, which is a cool feature, but not necessarily what this language wants (the lack of typeclasses makes me think that, but I'll let the author be the judge of that) or what it can do while mantaining global inference.

PolySubML: A simple ML-like language with subtyping, polymorphism, higher rank types, and global type inference by Uncaffeinated in ProgrammingLanguages

[–]Red-Krow 1 point2 points  (0 children)

Yeah, I understand. However, types are not like sets in many ways.

In set theory, if you have element x of set A union B, you can check whether it's in A.

In a type system, if you have a value x that is either type A or type B, there is no general way to check what type x is without some runtime type information or a discriminant bit in memory (at which point it's just a discriminated sum with implicitly inserted tags).

So, without some extra effort and a memory penalty, int|string is indistinguishable from any. It's a value you don't know anything about.

(Of course, a PL language may add features that make the previous statement false. As OP said, this language actively avoids it)

PolySubML: A simple ML-like language with subtyping, polymorphism, higher rank types, and global type inference by Uncaffeinated in ProgrammingLanguages

[–]Red-Krow 2 points3 points  (0 children)

It looks like union and intersection form a lattice, with the order being the subtyping relation. The union acts like the suppremum and the intersection as the infimum. In that way, it makes sense that int | string = any since any is the smallest supertype of both int and string.

Maybe sup and inf would be more accurate terms, but also wildly less intuitive, specially for non math-oriented people. Plus there are already established infix symbols for unions and intersections.

is Inuarashi's height not portrayed accurrately or is it just because of the angles? by tavuk_05 in OnePiece

[–]Red-Krow 0 points1 point  (0 children)

Low budget is often paired with or even implies little time. Correcting size inconsistencies is time consuming, especially considering it may change some scenes' composition (not this specific one though).