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
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
