notes on Ur/Web's fold function

This post is about Ur/Web Programming language at
http://www.impredicative.com/ur
it's a detail document on fold function, a type level folding function.

	Description	Example
val fold : K	a kind, one of Type, Name, or Unit.	Type
--> tf :: ({K} -> Type)	a type level function, given a record of K, return a Type,	con numFields = fn _ => int
	Following is a type level folder function.
	Given a value of type tf r, return a value of type tf ([ nm=v] ++r )
-> (nm :: Name ->	nm is a name,	Male
v :: K ->	v is a type of kind K,	bool
r :: {K} ->	rest of the record.	[ Name = string , Age = int]
[[nm] ~ r]	a prove of nm is not in r. The compiler will prove for you.	Prove of Male is not in { Name, Age}
=>	all arguments before => are type level, and can be deduced by compiler.
tf r ->	given a value of type tf r.	5
tf ([nm = v] ++ r))	return a value of type tf( [nm=v]++r)).	6
-> tf []	initial value, it has type tf [], [] is the empty record ( type level )	0
-> r ::: {K}	record to fold.	{ Name : "Alex", Age : 10 , Male : False}
-> folder r	a folder that will derived by the compiler
-> tf r	return type. eg. int	3