[Ur] Struggling to figure out mapping of record

[Simon Van Casteren]

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!

On Sat, Aug 18, 2018, 3:00 PM Adam Chlipala <adamc at csail.mit.edu> wrote:

> On 08/18/2018 08:43 AM, Simon Van Casteren wrote:
> > {Age: option float, FirstName: string}
> >
> > [...]
> >
> > {Age: option float -> either string int, FirstName: string -> either
> > string string}
> >
> > [...] Output should be of the type:
> >
> > {Age: either string int, FirstName: either string string}
> >
> > I feel Ur should be able to do it but I can't figure it out. I keep
> > going back to Top.map2, but there the "to" and "from" types should be
> > type level functions from a certain K to a and b, but my records are
> > monomorphic and don't really have any relation between them except for
> > the record of mapping functions.
>
> Actually, your records look like each field has a particular fundamental
> type pair, e.g. [option float] and [int] for [Age] and [string] and
> [string] for [FirstName].  So you can build a type-level record of pairs
> of types, that is, with kind [{(Type * Type)}], and use [map2] very
> naturally!
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20180818/202d1d73/attachment.html>