[Ur] How to specify Name to be a field of record?

[Adam Chlipala]

Vladimir Shabanov wrote:
> Hello. I'm trying to make some localized texts in my application. And
> I want this texts to be selected from record (so I can use same field
> name for html input id and text).
>
> I have code like this:
>
> val english_locale =
>      { EMail = "E-Mail"
>      , Keep  = "Keep me signed in"
>      , Password = "Password"
>      }
> val russian_locale =
>      { EMail = "E-Mail"
>      , Keep  = "Запомнить меня"
>      , Password = "Пароль"
>      }
>
> datatype language = En | Ru
>
> fun locale m =
>      case m of
>          En =>  english_locale
>        | Ru =>  russian_locale
>
> fun ltext m [s] = (locale m).s
>    

It's possible to implement a variety of equality-style constraints 
within Ur.  Here's one way of doing so to implement your example.

structure FieldOf : sig
     con fo :: Name -> Type -> {Type} -> Type
     val fo : nm ::: Name -> t ::: Type -> r ::: {Type} -> [[nm] ~ r] => 
fo nm t ([nm = t] ++ r)
     val proj : nm ::: Name -> t ::: Type -> r ::: {Type} -> fo nm t r 
-> $r -> t
end = struct
     con fo nm t r = $r -> t
     fun fo [nm] [t] [r] [[nm] ~ r] (x : $([nm = t] ++ r)) = x.nm
     fun proj [nm] [t] [r] (fo : fo nm t r) x = fo x
end

con locale = [EMail = string, Keep = string, Password = string]

fun ltext (m : language) [s :: Name] (fo : FieldOf.fo s string locale)
   = FieldOf.proj fo (locale m)

val example = ltext En [#Keep] FieldOf.fo