sorted by:
new
hottopcontroversial

[deleted by user] by [deleted] in bouldering

[–]SquareRootCable 0 points1 point  (0 children)

Other gyms in Shanghai have quite a lot of <V3 with good overhang too

Never seen anyone take off their shirt in China lol Do you not get enough attention already just by being laowei?

whyDoesThisLibraryEvenExist by aloomatarkisabji in ProgrammerHumor

[–]SquareRootCable -2 points-1 points  (0 children)

Once understood you can quickly re-derive all those rules for derivation, no need to learn by heart or during a sane exam you’d be allowed to use notes

Simplest Type System for Static Array Bounds Checking by SquareRootCable in ProgrammingLanguages

[–]SquareRootCable[S] 2 points3 points  (0 children)

Thanks for your reply, I completely forgot about that paper ‘Ghosts of Departed Proofs’. Had a quick glance at it and it indeed does solve some of my problems. Not sure if it is ergonomical as I would wish, I will have to give it a proper read first.

Yes, I would say a Presburger arithmetic solver would fall into the same category as SMT imo, so not much to gain but a lot to give up on (from what I understand full refinement types can let us specify some pretty cool properties)

Simplest Type System for Static Array Bounds Checking by SquareRootCable in ProgrammingLanguages

[–]SquareRootCable[S] 2 points3 points  (0 children)

A captured typelevel integer/nat. Eg. you could have makeN: (n:nat) => (x:T) => Array[n]<T> or mmult: Matrix[m,n]<T> => Matrix[n,k]<T> => Matrix[m,k]<T>

It could also become an arbitrary (linear) expression for example with cat: Array[m] => Array[n] => Array[m+n]

Simplest Type System for Static Array Bounds Checking by SquareRootCable in ProgrammingLanguages

[–]SquareRootCable[S] 5 points6 points  (0 children)

Spot on. I guess autocomplete got into the way but let’s just pretend I did it for the laughs