Designing programming languages is hard. I think every nontrivial programming language has at least a few "semantic messes"; even Scheme (R6RS) has a long specification with edge-cases (ex: https://www.r6rs.org/final/html/r6rs/r6rs-Z-H-6.html#node_se...). Meanwhile, C++ is a semantic mess that contains at least a few programming languages.
> if I had more experience implementing dependently typed languages, then perhaps I would not find it so weird, as it really just makes type constructors similar to functions, which they would be in a fully dependently typed language.
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.
> Yet an expression such as cols (replicate 0 (replicate 3 0)) should still work (and evaluate to 3)
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).
but that doesn't affect my point: cols has to know "something" about the name `replicate` more than just the types. why? because suppose i defined a function
def replicate5 n x = replicate 5 x
then
cols (replicate5 0 (replicate5 3 0)) == 5
that "something" is a shape function and now each data function must also correspond to a shape function. but that shape function doesn't magically have more info about its params than cols does about its params so you haven't solved any problem, you've just multiplied it.
spoiler alert every single tensor/array/matrix/ML/AI compiler runs into this same problem. there is only one solution: a fixed op set with a fixed number of corresponding shape functions. and then your compiler tries to perform shape inference/propagation. sometimes it works and you can specialize for fixed sizes and sometimes it fails and you get "dynamic" or "unknown" dims in your shapes and you can't do anything. oh well that's life in a universe where the halting problem exists.
Designing programming languages is hard. I think every nontrivial programming language has at least a few "semantic messes"; even Scheme (R6RS) has a long specification with edge-cases (ex: https://www.r6rs.org/final/html/r6rs/r6rs-Z-H-6.html#node_se...). Meanwhile, C++ is a semantic mess that contains at least a few programming languages.
> if I had more experience implementing dependently typed languages, then perhaps I would not find it so weird, as it really just makes type constructors similar to functions, which they would be in a fully dependently typed language.
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.
> Yet an expression such as cols (replicate 0 (replicate 3 0)) should still work (and evaluate to 3)
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
returns zero, but as described here 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).If I understand correctly,
would not typecheck, so I'm not sure I understand your example; could you clarify?okay i guess you're right since
but that doesn't affect my point: cols has to know "something" about the name `replicate` more than just the types. why? because suppose i defined a function then that "something" is a shape function and now each data function must also correspond to a shape function. but that shape function doesn't magically have more info about its params than cols does about its params so you haven't solved any problem, you've just multiplied it.spoiler alert every single tensor/array/matrix/ML/AI compiler runs into this same problem. there is only one solution: a fixed op set with a fixed number of corresponding shape functions. and then your compiler tries to perform shape inference/propagation. sometimes it works and you can specialize for fixed sizes and sometimes it fails and you get "dynamic" or "unknown" dims in your shapes and you can't do anything. oh well that's life in a universe where the halting problem exists.
[dead]