[Ur] Simple type level function Name -> Name - are there funnier examples?

[Adam Chlipala]

Marc Weber wrote:
> something more funny does no longer work:
>
> con change_name_toggle :: Name ->  Name = fn name =>
>      case name of
>            #Boo =>  #Bar
>            |#Bar =>  #Boo
>    

Yes, unlike Agda, Ur has separate languages for compile-time and 
run-time code.  You are trying to define a compile-time thing but using 
syntax that is only allowed for run-time code.

> So is there any way (more than one) to implement such function?
>    

I certainly hope not; that would break a nifty language property called 
"parametricity" which lets us deduce some specific properties of 
programs from their types.

> What else can be done with names? There are no operations such as
> "prefix them with db_" or such, are there?
>    

Correct.  The grammar of constructors in the manual gives a complete 
catalog of operations.