Re: [Ur] Struggling to figure out mapping of record

2018-08-18 Thread 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  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@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


Re: [Ur] Struggling to figure out mapping of record

2018-08-18 Thread Adam Chlipala

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@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


[Ur] Struggling to figure out mapping of record

2018-08-18 Thread Simon Van Casteren
Hi everybody, I'm struggling to get my validation functions the way I
really like them. What I would like to do is start from a record of input
fields that have a certain type, eg:

{Age: option float, FirstName: string}

I then have a function that will validate the values of this record, and
either return an error in the form of a string, or a type b, for every
field.

{Age: option float -> either string int, FirstName: string -> either string
string}

(either is just a sum type with two values Left and Right like in Haskell,
I should make a PR to get this into the stdlib, but that's not relevant
now).

How can I now apply this record of functions to this record of values?
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. (Not sure if all my terminology is correct here but I
hope you understand what I mean)

Any help much appreciated!

Simon
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur