Type theory friends: is there any work out there looking into the relationship between indexed inductive types and inductive recursive types?
Conversation
Replying to
For the specific use case I’m interested in, it seems like I can translate one into the other with wrapper types, but I’m curious if there’s anything more concrete. Both styles are convenient for different purposes.
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
Show replies
Replying to
I think these two are not really compatible..., or their common generalisation wouldn't make sense.
The following media includes potentially sensitive content. Change settings
View
1
1
Thanks, will have a look!