[Ur] exploring folders - I still don't get it.

Adam Chlipala adamc at impredicative.com
Mon Apr 16 07:55:40 EDT 2012


Marc Weber wrote:
> Trying to copy paste all the definitions which I think I need to make
> the countFields sample from the tutorial work into my own file and
> prefixing it by my_ yields this code, and the error shown at the bottom.
> Which magic is happening in the standard library I've missed?
>
> Also where exactly is the recursion (repeat until the attribute set has
> been processed) happening?
> Is it somewhere hidden in the compiler?

While [folder] is a type family that you can define yourself, folder 
_inference_ is built into the compiler and only applies to 
[Top.folder].  Your example doesn't specify a value of your own [folder] 
type, but the compiler won't infer such a thing.  The error message is a 
good one, to tell you that the function is only partially applied and 
isn't ready to yield an [int] yet.  (A "real" [folder] argument is 
implicit by default, but not so for your own type family.)

When the compiler synthesizes these values, they're built out of the 
combinators in [Top.Folder].  "The recursion" is encoded in the 
combinator tree, whose size varies with the size of the term to build a 
folder for.



More information about the Ur mailing list