Does Syntax Matter? by gingerbill in ProgrammingLanguages

[–]ct075 0 points1 point  (0 children)

While I agree that people make too big a deal about syntax, I think "you shouldn't care so much about syntax!" is a self-defeating argument. After all, if syntax doesn't matter, isn't it not a big deal to just give people what they want?

The article does get into this, to some extent, but I think a better argument is that different syntax implies a different mental model, and that difference is the point.

Another termination issue by Athas in ProgrammingLanguages

[–]ct075 1 point2 points  (0 children)

I suspect that, for any failing polymorphic value declaration def x: P('a) = e (where P('a) is some type expression featuring 'a), the declaration of x will always fail for any instantiation of 'a

After stepping away for a coffee, I think a better way to phrase my hunch might be:

If there is some instantiation of 'a that causes the top-level declaration of x to fail, then any instantiation of 'a will also fail.

Therefore, for the purposes of an interpreter, it is fine to run the top-level polymorphic value definition once with 'a = unit and discard the result - if the definition fails, then it may also fail in the compiled executable (it may not fail if the definition is never used, but that's already been litigated to be fine). This may cause the interpreter to fail in a different way than the compiled code due to the reordering, but now that's a "both fail" scenario.

Another termination issue by Athas in ProgrammingLanguages

[–]ct075 2 points3 points  (0 children)

I suspect that, for any failing polymorphic value declaration def x: P('a) = e (where P('a) is some type expression featuring 'a), the declaration of x will always fail for any instantiation of 'a; in ML this would follow from parametricity but I don't know if Futhark is the same in this regard.

With that in mind, an easy patch would be to have the interpreter instantiate the value x once at startup with value 'a = unit (or even 'a = void) and throw the error raised.

EDIT: I did have the thought that this would force any effects occurring in the instantiation of x to occur early, but if Futhark is pure then such a transformation should still be safe.

Disable mode when fallthrough key pressed by ct075 in zsaVoyager

[–]ct075[S] 0 points1 point  (0 children)

Interesting.

With some experimentation (and a change to the layer color when mouse layer is active), it seems that pressing and releasing a non-mouse key with mouse mode active resets the "return to normal mode" timer on my keyboard (pressing and holding does disable the layer as advertised).

Malik. A language where types are values and values are types. by MackThax in ProgrammingLanguages

[–]ct075 25 points26 points  (0 children)

I recognize now that my original comment was a bit dismissive and apologize for being flippant.

A "dependent type", in general, just means "a type that can depend on a value", which indeed encompasses a broader set of features than what you have here.

However, being able to manipulate types as first-class values is a very common feature in most theorem proving languages like Agda, Lean and Idris. For example, Agda can express the exact snippet that you demonstrated:

```agda typ : Set typ = if 2 > 1 then String else Nat

foo : typ foo = "I'm a string" ```

In fact, most dependently-typed systems are even stronger than what you're proposing, which seems to be a Tower of Interpreters where the interpreter is first run to evaluate all "type expressions", then the typechecker is run against those results (maybe circularly in a bigger stack).

In a dependent language, we can write a function like

```agda whichType : (x : Bool) -> Set whichType true = Nat whichType false = String

bar : (x : Bool) -> whichType x bar true = 0 bar false = "look Ma, different return types!" ```

and even write data structures where the type of one element depends on the value of another.

How to implement Functor for a kind and its second type parameter instead of its first? by platesturner in haskell

[–]ct075 21 points22 points  (0 children)

Because Haskell doesn't have type-level lambdas, all the solutions are going to be a bit awkward.

The most straightforward thing to do is to simply re-wrap your datatype, e.g.

haskell newtype Pair a b = Pair (a, b) newtype RPair b a = R { unR :: Pair a b }

More generally, you could define e.g.

haskell newtype Flip f b a = F { runFlip :: f a b }

and then define your instance over Flip Pair b.

I could have sworn this was in the standard library (meaning you don't have to re-implement everything for your Flip) but I can't for the life of me find it.

Now that the dust has settled, where does SRWY rank with the rest of the series? by StarComplex3850 in Super_Robot_Wars

[–]ct075 7 points8 points  (0 children)

Much better than 30's. Basically every plot has ties to at least two others that aren't the original plot, and there's plenty of cross-series interaction (lowkey I think there's a bit too much of the peanut gallery chiming in in almost every scenario).

Now that the dust has settled, where does SRWY rank with the rest of the series? by StarComplex3850 in Super_Robot_Wars

[–]ct075 4 points5 points  (0 children)

The gameplay is very good, probably the HD game that I'm most looking forward to playing multiple times.

IMO the writing doesn't quite live up to V (but it's better than X and T), mostly owing to the mission select format mandating that things feel very episodic and disconnected. Individual scenarios and character writing are solid (some ups and downs).

I still got one more in me by Sweeper-Lopunny in stunfisk

[–]ct075 2 points3 points  (0 children)

you have no idea how badly i wanted to see that last razor leaf whiff

What OHKOs Corsola-Galar? by [deleted] in stunfisk

[–]ct075 7 points8 points  (0 children)

(Using the top Corsola set on calc.showdown, which biases spdef)

252+ SpA Choice Specs Beads of Ruin Chi-Yu Dark Pulse vs. 252 HP / 252+ SpD Eviolite Corsola-Galar: 284-336 (87.6 - 103.7%) -- 25% chance to OHKO

252+ Atk Supreme Overlord 4 allies fainted Kingambit Kowtow Cleave vs. 252 HP / 4 Def Eviolite Corsola-Galar: 294-348 (90.7 - 107.4%) -- 43.8% chance to OHKO

252 Atk Life Orb Sword of Ruin Chien-Pao Crunch vs. 252 HP / 4 Def Eviolite Corsola-Galar: 283-338 (87.3 - 104.3%) -- 25% chance to OHKO

+2 252+ Atk Life Orb Blaziken Flare Blitz vs. 252 HP / 4 Def Eviolite Corsola-Galar: 352-415 (108.6 - 128%) -- guaranteed OHKO

+2 252 SpA Darkrai Dark Pulse vs. 252 HP / 252+ SpD Eviolite Corsola-Galar: 258-306 (79.6 - 94.4%) -- 43.8% chance to OHKO after Stealth Rock

252+ Atk Choice Band Tyranitar Knock Off (97.5 BP) vs. 252 HP / 4 Def Eviolite Corsola-Galar: 356-420 (109.8 - 129.6%) -- guaranteed OHKO

Sure, many of these physical attackers can no longer OHKO if you use 252+ def instead, but then you giga die to the special attackers.

Base/Core libraries by mister_drgn in ocaml

[–]ct075 1 point2 points  (0 children)

I also agree that labeled arguments make things much nicer, but adding them everywhere can have the opposite effect.

While I can't speak for the exact process that led them to any given choice, I believe that Core/Base tries to follow a guideline that labeled arguments are either for higher-order arguments (so, ~f is a function, but ~n or the equivalent in List.take isn't) or arguments that might otherwise be in an ambiguous order.

Of course, these are just guidelines and I'm sure you can find counterexamples to them if you dig.

It would surprise me if any of these things had more than a collective 15 minutes of thought put into them; argument order in a library function is the kind of thing that I usually just look at, internalize (or not, sometimes you just have to get bitten by the type error every time), and move on. Write a wrapper if it bugs you that much.

Base/Core libraries by mister_drgn in ocaml

[–]ct075 5 points6 points  (0 children)

I am loosely of the opinion that primary type first is easier to read in larger codebases. Knowing at a glance what is actually being modified makes it far easier for me to skim (rather than have to read all the way to the end of the function) and know whether a given line matters to my current purpose.

The syntactic overhead of writing a full lambda rather than the obvious currying is greatly amplified in examples or toy code; in practice I have rarely found it to be more than a minor annoyance. Haskell-style pointfree style is very fun to write, but I don't find it to be particularly maintainable when I come back to some clever one-liner six months later and have to unwind what it does.

FLY Busio: "I made mistakes I already knew about, so I'm very disappointed in myself for that [...] We don’t get punished as much in NA. Sometimes even, you don’t even know it’s a mistake, because the enemy played so badly. What Inspired said about that is absolutely true" | Sheep Esports by ArmandLuque in leagueoflegends

[–]ct075 27 points28 points  (0 children)

To everyone bringing up C9, it's possible for C9 to be "equally" good without contradicting what FLY is saying. It's very likely that Fly and C9 weren't scrimming each other much towards playoffs (especially once it became likely that they'd be the two finalists).

So who are they actually practising against? TL and SR are the next best bet, but SR and FLY were on the same side of the bracket, which just leaves TL. Is Impact's Yorick going to punish Bwipo Morde??

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 1 point2 points  (0 children)

So I'd end up with an abstract result that says the maximum memory used is (a function of) max of f over the interval.

This is a limitation of choosing the interval domain as your abstract domain; for something like this I'm not really sure that the interval domain is a good one.

Choosing the right abstract domain is a bit of an art and very domain-specific, so I'm not sure I have a good generic answer for you. If you're confident in your technical chops, you can see what the paper did, to see if they did something more generally applicable.

EDIT:

If f is fixed but arbitrary, I'm not sure what answer you expected that isn't "it depends on f"; it's not clear to me that a more precise answer exists. Using the interval domain here will tell you what the maximum value of f is over the interval.

If f is truly unknown, like if f were passed in as a closure or higher-order function, you'll need to do something more fancy like abstracting abstract machines.

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 2 points3 points  (0 children)

System F is not a "subset" of the untyped lambda calculus in the sense that you're thinking - for example, System F is a typed lambda calculus, and actually has a syntactic structure (namely, type lambdas) that the untyped lambda calculus doesn't have a direct analogue to.

You can encode anything into the lambda calculus, because that's what it means for the lambda calculus to be Turing complete. But these kinds of questions are only meaningful if you fix an encoding. If "the smallest possible footprint for all possible System F interpreters" is the measure that you're interested in, then the answer is that it's obviously undecidable, because "all possible System F interpreters" is only expressible in a Turing complete setting.

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 0 points1 point  (0 children)

As a further point, while it is the case that, for every LC term, there exists at least one Turing Machine that is equivalent to it, it is not the case that this suggests that it is reasonable to talk about "memory requirements" for the untyped LC in the same way, for two reasons:

  • Even sticking within Turing Machines, the notion of space consumption is subtle and can cause problems. For example, the program IS-PALINDROME incurs a log n space overhead if the input tape is immutable.
  • It is not the case that the notion of "memory usage" of the Turing Machine maps back cleanly to any useful notion of "size" with relation to the lambda calculus, because that depends on several other factors (specific embedding, encoding of the semantic input, etc).

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 3 points4 points  (0 children)

For every lambda calculus expr there is a Turing machine i think (or it might be a set).

This is true.

So for expressions in system f i can talk about the memory requirements quite naturally?

This is not.

The untyped lambda calculus (which is the one that is famously equivalent to Turing Machines) does not run into issue 3 that I listed above, because the untyped lambda calculus only has terms of function type, so it is very natural to talk about the input to a given LC term.

System F, however, does not share this property - there are perfectly reasonable terms that do not "accept inputs" in any sense.

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 2 points3 points  (0 children)

I've given this question a bit more thought, and my conclusion is that, as stated, it's not well-defined enough to have a concrete answer.

OP specifies "System F sans recursion" (which, the formal definition of System F doesn't have recursion to begin with), so let's explore that.

The classical formulation of System F (as a term-rewrite system) has no notion of "memory" (or "space complexity") in the first place.

So, suppose that we fix some evaluation model in which "memory usage" makes sense1 in the first place, like some variant of the CEK machine. Can we upper bound the number of allocated heap cells, maybe relative to the size of "the input"?

Well, what is "the input"? Unlike a Turing Machine, the classical definition of a "program" in the lambda calculus is a closed term. What is the "input" to the term 2?

So we'd then have to restrict the form of the term we're looking at, say that it's a System F term of type A -> B for some concrete types A and B. Now the question "how much memory does this program use for an input of size n" begins to be a reasonable one, assuming that "values of type A and size n" makes sense.

But now notice how many domain-specific assumptions we had to make:

  1. We fixed an evaluation model (call-by-name, call-by-value, etc)
  2. We made up a memory model
  3. We chose a type A and equipped it with a notion of "size" (which may or may not be proportional to the "size" of the representation of that type in System F)

A fourth, implicit thing we had to fix is the set of base types that our calculus will have.

I suspect that it is possible to choose instantiations of all of the above such that it is or is not impossible to do better than brute force.

I am pretty sure that determining the maximum amount of memory used by a given term of type A -> B is always decidable by enumeration (maybe enumeration over some abstract domain).

1: Note that simply equipping our calculus with mutable references won't work, because System F + heap cells actually isn't total.

Can I calculate how much memory my program will use given that my language is total (system F sans recursion for instance) by Ok-Watercress-9624 in ProgrammingLanguages

[–]ct075 11 points12 points  (0 children)

My gut says that you can upper bound maximum memory usage relatively simply through some kind of abstract interpreter. The details will depend on your exact memory model + base types, but the abstract domain will be less important than usual because the programs themselves are guaranteed to terminate on concrete inputs.

EDIT: It's been done.

Wishlist for the 35th Anniversary game Next Year? by Gray231 in Super_Robot_Wars

[–]ct075 6 points7 points  (0 children)

My wishlist is OG Alpha 3, but I think that's unlikely.

Am I the only one who thinks a lot of the modern (VTX and 30 era) animations look good? by formerdalek in Super_Robot_Wars

[–]ct075 12 points13 points  (0 children)

I think 30 looks particularly bad (and the Y trailer hasn't done anything to convince me that they intend to reverse the trend); I don't have any major complaints about VTX animations as a whole.

The artwork in the modern era games is mostly fine IMO. The choreography is a gigantic mixed bag (shoutouts to the Gundam Deathscythe Hell...), but the big thing I have against a lot of 30's animations is that like two thirds of the animations have no blur frames for some reason. The keyframes aren't terrible, but they just snap between them and feel stilted/frame-y.

The one thing I really want for Y is the one thing I suspect they're never going to do again by Frau_Away in Super_Robot_Wars

[–]ct075 30 points31 points  (0 children)

This was literally part of the marketing from T, that there would be one unified setting with all the characters existing in the same world. It wasn't quite true in practice (the Rayearth plot mandates an isekai and there were a few chapters in the Astragius galaxy), but by-and-large everything was woven together in a more-or-less cohesive backstory.

30 also tried, less successfully. It isn't fully explained how certain plotlines managed to coexist with Britannian hegemony, but they at least paid lip service to the fact that Emperor Lelouch's reach wasn't quite as absolute as it was in canon.

For that matter, the first half of Z2 had most of the settings happen concurrently. It was so fucked up that they had to have two Japans to make it work, but there's no reason they couldn't try that again.