type error when min of empty set under catch undef

[SaadAttieh]

find a : int(1)

such that catchUndef(min({}), -1) = -1
such that catchUndef(max({}), -1) = -1

output:

Generating models for test2.essence
Error 1:
    In a 'such that' statement: catchUndef(min({}), -1) = -1
    Error:
        Type error in min({})
                      Unexpected type inside min: set of ?
Error 2:
    In a 'such that' statement: catchUndef(max({}), -1) = -1
    Error:
        Type error in max({})
                      Unexpected type inside max: set of ?

[ott2]

Isn't this just the usual issue about empty set not having a type? It can be coerced to have a type via something by giving it a provenance something like {0} intersect {1}, and perhaps also using the backtick notation that I never remember?

[SaadAttieh]

Conjure should be able to deduce the inner type from the context it was used in. For example it works fine if you write min of empty set when not under the catch undef. I was extending Athanor to do the same and added this to Athanor's tests but discovered that for some reason (assuming something simple), it does not work under the catch undef.

On 23 Jul 2019, at 12:39 pm, András Salamon [email protected] wrote:

Isn't this just the usual issue about empty set not having a type? It can be coerced to have a type via something by giving it a provenance something like {0} intersect {1}, and perhaps also using the backtick notation that I never remember?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ozgurakgun]

I actually never intended catchUndef to be used in the input, but didn't disallow it either. This should be easy to fix, but it will have to wait until next week when I am back.

[SaadAttieh]

Cheers! Could we make catchUndef officially be part of Essence input? I've actually needed it in some of my specs and so Athanor actually supports it. Well tbh the only place I use it is when needing to catch min/mmax of a list which should be allowed to be empty. On 23 Jul 2019, at 9:14 pm, Özgür Akgün [email protected] wrote:

I actually never intended catchUndef to be used in the input, but didn't disallow it either. This should be easy to fix, but it will have to wait until next week when I am back. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ott2]

Agree with Saad, also catchUndef makes for interesting semantics. :-)