4 ms·

I have a tangential question that is related to this cool new feature. Warning: the question I ask comes from a part of my brain that is currently melted due t

by aeonik 3y ago

I have a tangential question that is related to this cool new feature. Warning: the question I ask comes from a part of my brain that is currently melted due to heavy thinking. Context: I write a fair amount of Clojure, and in Lisps the code itself is a tree. Just like this F# parallel graph type-checker. In Lisps, one would use Macros to perform compile-time computation to accomplish something like this, I think. More context: Idris2 allows for first class type-driven development, where the types are passed around and used to formally specify program behavior, even down to the value of a particular definition. Given that this F# feature enables parallel analysis, wouldn't it make sense to do all of our development in a Lisp-like Trie structure where the types are simply part of the program itself, like in Idris2? Also related, is this similar to how HVM works with their "Interaction nets"? https://github.com/HigherOrderCO/HVM https://github.com/HigherOrderCO/HVM https://www.idris-lang.org/ https://www.idris-lang.org/ https://clojure.org/ https://clojure.org/ I'm afraid I don't even understand what the difference between code, data, and types are anymore... it used to make sense, but these new languages have dissolved those boundaries in my mind, and I am not sure how to build it back up again.

Arelius 3y ago
> Given that this F# feature enables parallel analysis, wouldn't it make sense to do all of our development in a Lisp-like Trie structure where the types are simply part of the program itself, like in Idris2? Yeah, maybe, you for sure could, but in the context of F# as it exists, it may be hard to get from here to there. > 'm afraid I don't even understand what the difference between code, data, and types are anymore... it used to make sense, but these new languages have dissolved those boundaries in my mind, and I am not sure how to build it back up again. Yeah, good luck with that. I think maybe taking a mental step away from programing might help. It's true that human interpretation of the world often has these properties. And he generalization of the systems in no way invalidate the usefulness of the categorization system. Maybe it's helpfulnto consider the properties of your classes. To risk your further descent into madness. I recommend the Lambda days talk on the Verse programming language [1]. Which has further contemplation on the topics you are thinking about. With an eye towards practicality. [1]: https://youtu.be/OJv8rFap0Nw?si=XvUoBqO7IeCLIbrn https://youtu.be/OJv8rFap0Nw?si=XvUoBqO7IeCLIbrn

by aeonik 3y ago

Arelius 3y ago

> Given that this F# feature enables parallel analysis, wouldn't it make sense to do all of our development in a Lisp-like Trie structure where the types are simply part of the program itself, like in Idris2? Yeah, maybe, you for sure could, but in the context of F# as it exists, it may be hard to get from here to there. > 'm afraid I don't even understand what the difference between code, data, and types are anymore... it used to make sense, but these new languages have dissolved those boundaries in my mind, and I am not sure how to build it back up again. Yeah, good luck with that. I think maybe taking a mental step away from programing might help. It's true that human interpretation of the world often has these properties. And he generalization of the systems in no way invalidate the usefulness of the categorization system. Maybe it's helpfulnto consider the properties of your classes. To risk your further descent into madness. I recommend the Lambda days talk on the Verse programming language [1]. Which has further contemplation on the topics you are thinking about. With an eye towards practicality. [1]: https://youtu.be/OJv8rFap0Nw?si=XvUoBqO7IeCLIbrn https://youtu.be/OJv8rFap0Nw?si=XvUoBqO7IeCLIbrn