I am always needing sized types I wish they were real

@amy actually while I'm here. what kind of inductive type do you want it for? more specifically does your inductive type X have recursive arguments of type (B -> X) or are they all just shaped mostly like X (up to indices, I guess)

@amy ok this supports my hypothesis that in most use cases ppl don't actually need infinitary sizes

@amy "most people" being "PL academics working with ASTs"

@ionchy maybe instead of sized types i should just add a pragma or something

@amy Agda pragmas starting to look like GHC extensions

@ionchy traverse is guardedness-preserving in its kth argument or something

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.