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
Replying to
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
The `Format` version is very convenient but in some cases I’d like to be able to constrain a format to a specific representation, eg. `FormatOf A`.
1
An am also pondering tracking the sizes of formats as well, which could start getting unwieldy for my poor users with indexed types.
1
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
Show replies