Type theory friends: is there any work out there looking into the relationship between indexed inductive types and inductive recursive types?
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Thanks, I'll have a look!
For me the case is I have a universe of binary format descriptions, and an associated family of in-memory representations of those format descriptions:
Format : Type
Repr : Format -> Type
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Ahh will have to ponder the implications of that but that’s useful knowledge to know. Am currently sketching it out using Idris 2 as a logical framework which doesn’t yet keep me honest bout such stuff. Maybe I should switch to Agda 😅
1
I think it should probably be alright though.
1
There’s might be some exotic use cases of meta-formats that can describe other formats, but from that I think I can start to get an inkling about why you’d need to be careful about this stuff.
1
1
At any rate I think keeping representation types small is a decent restriction, and one I had planned to do anyway come to think of it.