@a_cowley @aaronmblevin @viktorklang if I had DTs, I'd express reflection as universe code and proof that interp of code is iso to your type
-
-
Replying to @copumpkin
@a_cowley@aaronmblevin@viktorklang in the sense used in https://www.andres-loeh.de/DGP-Agda.pdf and similar. You can reflect only a particular universe3 replies 0 retweets 2 likes -
Replying to @copumpkin
@copumpkin@aaronmblevin@viktorklang Isn't the iso you want a bit tricky? [[C]] ~ T, can the type checker generate that proof?1 reply 0 retweets 0 likes -
Replying to @a_cowley
@a_cowley@aaronmblevin@viktorklang it's pretty mechanical/annoying. I'd think of it working like GHC generates Generic instances today.1 reply 0 retweets 0 likes -
Replying to @copumpkin
@copumpkin@aaronmblevin@viktorklang Yeah, I'm just worried the generic library author would need to provide helpers for witness generation1 reply 0 retweets 0 likes -
Replying to @a_cowley
@a_cowley@aaronmblevin@viktorklang oh, I'd build the basic universe generation code into the compiler. Generics libraries would consume it1 reply 0 retweets 0 likes -
Replying to @copumpkin
@copumpkin@aaronmblevin@viktorklang Wouldn't that make it harder to slice off more limited families of types?1 reply 0 retweets 0 likes -
Replying to @a_cowley
@a_cowley@aaronmblevin@viktorklang your library would have a decision procedure translating big universe to smaller one, preserving iso2 replies 0 retweets 1 like -
Replying to @copumpkin
@copumpkin@aaronmblevin@viktorklang Got it. Please submit a GHC PR that scraps most of the meta programming facilities in favor of this
.1 reply 0 retweets 4 likes -
Replying to @a_cowley
@a_cowley@aaronmblevin@viktorklang perhaps@edwinbrady has something similar in mind for Idris :)1 reply 0 retweets 0 likes
@copumpkin @a_cowley @aaronmblevin @viktorklang perhaps in version 2...
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.