On Mon, Jan 4, 2021 at 9:20 AM Volker Dobler <[email protected]> wrote:
> On Sunday, 3 January 2021 at 18:43:22 UTC+1 [email protected] wrote: > >> I do believe (hope) David was kidding. Anonymous product types (and >> similar constructs) are the root of all evil. >> > > Yes, you need dependent product types. Especially anonymous ones. > Haha! It would be quite the effort to add those. You need a partial evaluator for your language in order to solve equality questions in the type system. The slightly serious part though is that if you want to handle tensor algebras correctly you are probably looking at either full dependent types or a large subset thereof which works on arithmetic (I believe a lot of research was done by Frank Pfenning and Hongwei Xi in the arithmetic-only area. Also see the ATS language). To be even more serious, you probably want the dual construction, namely dependent sums. They generalize product types. There's a similarity of those to Go's interfaces though with some subtle differences. Most importantly, interfaces are "opaque" in that they only concern themselves about behavior and not the actual underlying interface type. Whereas in a dependent sum you have "transparency" in that you do get to access and exploit the underlying type. For abstraction you want the opaqueness. -- J. -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAGrdgiUeDRoet3DXNkwUQorJ8WD82Q16j3ZJLvPsmTK4A1kD6g%40mail.gmail.com.
