Since the new HF ED’s experience in this matter has generated renewed interest:
We need to acknowledge that people are used to the dichotomy between values and types.
…or maybe even prefer their separation. But I have been wrong before, and maybe e.g. Ohmu was just “ahead of its time”.
From BTG 2020-12-02:
-
Overcoming Stereo types: Using type-level programming in Haskell to parse tricky JSON
-
[in the “Loco-motive” article]
Dependent types exist for a while in other programming
languages, for instance, Agda, Idris, Coq, etc. They are known to be used mostly in research areas (for writing proofs) or in verification systems where it is crucial to get everything correct (e.g. aeroplane software).
…did we choose the wrong paradigm - should we be using languages based on e.g. predicate logic instead of higher-order functions? At least then the difference between types and values would be much smaller: we could use Prolog for both.