Anonymous
6/12/2025, 7:12:06 PM
No.105573196
>>105564145
I recently read through the little typer and would highly recommend it. Dependently typed functional programming and untyped programming shares the same relationship in my mind as conservative vector fields to non-conservative fields. Technically a non-conservative vector field doesn't exists and you could model any problem using only conservative fields if you are willing to include enough variables, but you're not so you model using non-conservative fields. Similarly if you want to program like this you have to arity of your types must match the arity of the problem domain exactly. Once you've modeled your types correctly the logic is really easy and natural.
I recently read through the little typer and would highly recommend it. Dependently typed functional programming and untyped programming shares the same relationship in my mind as conservative vector fields to non-conservative fields. Technically a non-conservative vector field doesn't exists and you could model any problem using only conservative fields if you are willing to include enough variables, but you're not so you model using non-conservative fields. Similarly if you want to program like this you have to arity of your types must match the arity of the problem domain exactly. Once you've modeled your types correctly the logic is really easy and natural.