Jon Sterling on Nostr: I don’t like that in proof assistants and programming languages, we take everything ...
I don’t like that in proof assistants and programming languages, we take everything we know about programmers’ intentions (i.e. how they are thinking about the *purpose* or *role* of some data of operation), and throw it on the floor, and then perhaps later on try and put humpty-dumpty back together again using higher-order unification.
An early example of NOT doing this and instead reifying programmer’s intentions is in Epigram, where nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqw4y42l2xu0p3a9yrfecmmsmlvhzrk3xe67vp0gpfw55q8s3kz2hs426al5 (nprofile…6al5) taught us the “labelled types” trick, which works surprisingly well for making sense of definitions of function even without the special syntactic support for which Epigram was well known.
I intend to do the same with algebraic structures. There is no reason we must push our whole brain through the pinhole of unification against carrier sets. More on this later ;-)
An early example of NOT doing this and instead reifying programmer’s intentions is in Epigram, where nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqw4y42l2xu0p3a9yrfecmmsmlvhzrk3xe67vp0gpfw55q8s3kz2hs426al5 (nprofile…6al5) taught us the “labelled types” trick, which works surprisingly well for making sense of definitions of function even without the special syntactic support for which Epigram was well known.
I intend to do the same with algebraic structures. There is no reason we must push our whole brain through the pinhole of unification against carrier sets. More on this later ;-)