Does anyone know why Wadler&#39;s &quot;Recursive Types for Free&quot; techniques are not used more widely, for example in Agda? Is it because of the inefficiency of execution?<div>- Anthony</div>