by jmillikin on 10/2/25, 12:38 AM with 8 comments
by armchairhacker on 10/2/25, 2:39 AM
by almostgotcaught on 10/2/25, 1:28 AM
Denotational or operational semantics: pick one for your programming language and stick to it. The author (who I generally think is very smart) here is striving for denotational semantics (type level data) and trying to torture the operations into supplying the appropriate result. Operationally `cols (replicate 0 (replicate 3 0))` is 0 not 3. So now you have to bend over backwards and implement custom shape functions that not only return weird answers but have to be special cased AND context sensitive - ie without trying the language I'm 100% sure that
cols (replicate 0 "x")
returns zero, but as described here cols (replicate 0 (replicate k "x"))
returns k. Ie cols has to introspect semantically into its argument. That's not just tedious, it's impossible unless you don't let people add names that can participate (ie arbitrary functions). Or you ask them to implement the same shape functions (which doesn't solve the problem because they'll be no more equipped than you are).by lmm on 10/2/25, 1:15 AM
Yeah. I was screaming for most of this piece, because this all seems like standard dependently-typed stuff, and ironically enough implementing full dependent types would probably end up being easier than trying to handle this one feature as a special case.
by Ferret7446 on 10/6/25, 3:40 AM