<div dir="auto">It's so hard to think on this "level" for me. But I got it working! The approach is obvious now that you told me, but I've spent many hours thinking about it. Thanks so much for the help! </div><br><div class="gmail_quote"><div dir="ltr">On Sat, Aug 18, 2018, 3:00 PM Adam Chlipala <<a href="mailto:adamc@csail.mit.edu">adamc@csail.mit.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 08/18/2018 08:43 AM, Simon Van Casteren wrote:<br>
> {Age: option float, FirstName: string}<br>
><br>
> [...]<br>
><br>
> {Age: option float -> either string int, FirstName: string -> either <br>
> string string}<br>
><br>
> [...] Output should be of the type:<br>
><br>
> {Age: either string int, FirstName: either string string}<br>
><br>
> I feel Ur should be able to do it but I can't figure it out. I keep <br>
> going back to Top.map2, but there the "to" and "from" types should be <br>
> type level functions from a certain K to a and b, but my records are <br>
> monomorphic and don't really have any relation between them except for <br>
> the record of mapping functions.<br>
<br>
Actually, your records look like each field has a particular fundamental <br>
type pair, e.g. [option float] and [int] for [Age] and [string] and <br>
[string] for [FirstName].  So you can build a type-level record of pairs <br>
of types, that is, with kind [{(Type * Type)}], and use [map2] very <br>
naturally!<br>
<br>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank" rel="noreferrer">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer noreferrer" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote></div>