function types restricting tagged types?

[Chris Cannam]

If I give a function an explicit type, it restricts the types accepted
as arguments (provided it's compatible with the inferred type for the
function). For example,

> f x = x
<code$f> is 'a -> 'a
> f x is number -> number = x
f is number -> number = <code$f>

But this doesn't seem to work as expected with variant types:

> f = \case of X _: println "it's an X"; Y _: println "it's a Y"; _: () esac
f is X 'a | Y 'b -> () = <code$>
> g val is (X number) -> () = f val
g is X number | Y 'a -> () = <code$g>

Why is this? I had expected g to accept only X tags.


Chris

[Madis]

On Thu, 17 Jan 2013, Chris Cannam wrote:

> But this doesn't seem to work as expected with variant types:
>
>> f = \case of X _: println "it's an X"; Y _: println "it's a Y"; _: () esac
> f is X 'a | Y 'b -> () = <code$>
>> g val is (X number) -> () = f val
> g is X number | Y 'a -> () = <code$g>
>
> Why is this? I had expected g to accept only X tags.

There are two kinds of variant tags at type level - constructor value
variant (like the is X number in your example), and accepted value variant
(the ones accepted by a case expression).

The difference between the variant tags is that constructor one can be
extended (and only extended) - for example you have [A 1] ++ [B true] and
the unification on ++ arguments extends A number with B bool into
A number | B boolean. It cannot be narrowed, as it would mean ignoring
possible actual value reprented by the type.

The accepted variants on the other side can be narrowed, but not extended
- for example if you write a case expression:
f = \case of
A n: n + 1;
B t: if t then 1 else 0 fi;
esac;

then it accepts A and B but nothing else. Unification of f type
(A. number | B. boolean) -> number with another function
(A. number | C. string) -> number will result in narrowed variant type
A. number -> number, since that's the only variant always accepted. The
accepted types cannot be extended - it would mean declaring that you
accept a value, that actually is not accepted by some branch of the code.

Unification between accepted and constructed variant types creates a
frozen variant type matching the constructed type. It cannot be either
extended nor narrowed any more.

Now you have the any match (_:) in the case - which causes case to accept
any tag you throw at it, and this is represented at type level as using
the constructor value type tags instead of accepted tags (as it accepts
anything). The side effect is, that unlike the normal case variant type,
it cannot be narrowed anymore. Had the any variant been missing, your
example would have worked with accepted variant type declaration:

> f = \case of X _: println "it's an X"; Y _: println "it's a Y"; esac
f is X. 'a | Y. 'b -> () = <code$>
> g val is (X. number) -> () = f val
g is X. number -> () = <code$g>

Note the dots after variant tags in types - these mark accepted variants.

[Chris Cannam]

On 17 January 2013 22:21, Madis <ma...@cyber.ee> wrote:
> Now you have the any match (_:) in the case - which causes case to accept
> any tag you throw at it, and this is represented at type level as using the
> constructor value type tags instead of accepted tags (as it accepts
> anything). The side effect is, that unlike the normal case variant type, it
> cannot be narrowed anymore.

So although you can narrow the type for a case that accepts X or Y by
removing Y to give X only, if the case accepts anything, it cannot be
narrowed by removing Y because (anything - Y) is not meaningful as a
set of variant types? (i.e. it would mean you had to anticipate all
possible variants.) Do I have this right?

> Had the any variant been missing, your example
> would have worked with accepted variant type declaration:

That makes sense, thanks.

I've got used to writing the extra _: alternative in my case
expressions because of the way lists are handled:

> f = \case of h::t: println "not empty"; []: println "empty" esac
1:6: Partial match: []

> g is X. number -> () = <code$g>
>
> Note the dots after variant tags in types - these mark accepted variants.

Is there a reference for what these annotations mean? I found "^"
(sortable type) by reading the source code, and from somewhere I got
the impression that ` indicates a constructed type, but it's all a
bit... osmotic.


Chris

[Madis]

On Thu, 17 Jan 2013, Chris Cannam wrote:

> On 17 January 2013 22:21, Madis <ma...@cyber.ee> wrote:
>> Now you have the any match (_:) in the case - which causes case to accept
>> any tag you throw at it, and this is represented at type level as using the
>> constructor value type tags instead of accepted tags (as it accepts
>> anything). The side effect is, that unlike the normal case variant type, it
>> cannot be narrowed anymore.
>
> So although you can narrow the type for a case that accepts X or Y by
> removing Y to give X only, if the case accepts anything, it cannot be
> narrowed by removing Y because (anything - Y) is not meaningful as a
> set of variant types? (i.e. it would mean you had to anticipate all
> possible variants.) Do I have this right?

Not exactly, the reason is that allowing anything means that the set is
extensible, and narrowing extensible variant sets is not allowed, as it
may discard constructed value tags. OCaml seems to do exactly the same
thing, and it is an easy solution that results in sound typesystem
(although restricting some valid code). Maybe a special variant set kind
could be used for case expressions accepting anything, but I haven't
thought very thoroughly about it.

>> g is X. number -> () = <code$g>
>>
>> Note the dots after variant tags in types - these mark accepted variants.
>
> Is there a reference for what these annotations mean? I found "^"
> (sortable type) by reading the source code, and from somewhere I got
> the impression that ` indicates a constructed type, but it's all a
> bit... osmotic.

'a and ^a are free type variables, and yes ^ means restricted to ordered
types.

` is used on variant tags and structure field names to mean the "frozen"
variant/field which is both required by some variant constructor/field
reference and accepted by variant case or struct constructor (struct and
variant types act as mirrors).
. is used to describe variant tag or struct field where value is used by
some code (like field selector or case expression). The constructed value
fields/tags are not marked specially.

Yes the typesystem should be described more throroughly (probably in
some separate typesystem reference).

[chrisichris]

Now you have the any match (_:) in the case - which causes case to accept
any tag you throw at it, and this is represented at type level as using
the constructor value type tags instead of accepted tags (as it accepts
anything). 

Oh that sounds nice for passing an options-list to functions where the functions passes some options further to another functions which demands some different options 

fn1 opts =

   (var o1 = 0;

   for opts \case of

               O1 v: o1 := v;

               _ = ();

               esac;

   println o1);

fn2 opts =

   (var o2 = 0;

   for opts \case of

               O2 v: o2 := v;

               _ = ();

               esac;

   fn1 opts;

   println o2);

fn2 [O1 1, O2 2];

Should work than right?

Unitl now I have always used thwo lists for that similar eval.evaluteYetiCode

    

[Chris Cannam]

On 18 January 2013 03:10, Madis <ma...@cyber.ee> wrote:
> Maybe a special variant set kind could be used
> for case expressions accepting anything, but I haven't thought very
> thoroughly about it.

I wonder how best to handle the situation where I have relatively many
variant tags coming into a function, and at one point I want to handle
only one of them in a different way from the others.

That is, to do something like

case x of
A a: println "special-casing this one";
_: println "normal case";
esac

without having to list all possible A, B, C etc as separate cases or
accidentally widening the function type. Is there any way?


Chris

[Madis]

On Fri, 18 Jan 2013, chrisichris wrote:

> Oh that sounds nice for passing an options-list to functions where the functions passes some
> options further to another functions which demands some different options 
>
> fn1 opts =
>    (var o1 = 0;
>    for opts \case of
>                O1 v: o1 := v;
>                _ = ();
>                esac;
>    println o1);
>
> fn2 opts =
>    (var o2 = 0;
>    for opts \case of
>                O2 v: o2 := v;
>                _ = ();
>                esac;
>    fn1 opts;
>    println o2);
>
> fn2 [O1 1, O2 2];
>
> Should work than right?
>
> Unitl now I have always used thwo lists for that similar eval.evaluteYetiCode

It should work. It also allows any option to be given, which can imho easily result in bugs.

fn2 [OI 1];

[chrisichris]

It should work. It also allows any option to be given, which can imho easily result in bugs.

fn2 [OI 1];

Right so the two args for two option-lists is obviously better (and not much different) 

[Madis]

I now implemented a bit smarter handling of such case expressions type -
it basically still gets extendable variant type, but flagged as also
narrowable. Seems like it should work.

> f = \case of B (): println "!!!"; _: () esac
f is B () -> () = <code$>
> g x = (println case x of A x: x; B (): "B" esac; f x);
g is A. string | B. () -> () = <code$g>
> g is (A. string) -> ()
<code$g> is A. string -> ()
> f is (A. string) -> ()
<code$> is A. string -> ()

The last one restricts the f to type that is accepted only by default
match - probably not very useful, but well, the function actually accepts
A-tagged variants (although not doing anything with them), so it is valid
code from compilers point-of-view.

[Chris Cannam]

On 22 January 2013 01:41, Madis <ma...@cyber.ee> wrote:
> I now implemented a bit smarter handling of such case expressions type - it
> basically still gets extendable variant type, but flagged as also
> narrowable.

Ooh, interesting!

This certainly seems to do the job in the test case in front of me
now, and I have a few more situations coming up where it would be
useful. Thanks for that -- I just hope it doesn't turn out to have
introduced any nasty holes.


Chris

[Chris Cannam]

On 22 January 2013 01:41, Madis <ma...@cyber.ee> wrote:

> I now implemented a bit smarter handling of such case expressions type - it
> basically still gets extendable variant type, but flagged as also
> narrowable. Seems like it should work.

At the time I said that this seemed to work -- but I think I may have
been checking too superficially.

>> f = \case of B (): println "!!!"; _: () esac
> f is B () -> () = <code$>
>> g x = (println case x of A x: x; B (): "B" esac; f x);
> g is A. string | B. () -> () = <code$g>
>> g is (A. string) -> ()
> <code$g> is A. string -> ()

But now:

> g (B ())
B
!!!
>

in other words, the compiler reports the narrowed type but still
accepts the wider type.

It seems to do this for any function that accepts variant types
regardless of whether there are any constructed types involved:

> f x is (A number | B number) -> 'a = x
f is A number | B number -> A number | B number = <code$f>
> f (C 1)
C 1 is A number
| B number
| C number
>

This can also lead to run-time type errors, for example using the
default branch of https://bitbucket.org/cannam/yertle:

> store = load yertle.store
> s = store.newStore ()
s is [yertle/store:store]<> = {indexes=[{order=[0,1,2],
tree=[:]},{order=[1,2,0], tree=[:]},{order=[2,1,0], tree=[:]}]}
> store.match
<yertle.store$match> is [yertle/store:store]<> -> {
o is Known (Blank number
| IRI string
| Literal {
language is string,
type is string,
value is string
}) | Wildcard (),
p is Known (IRI string) | Wildcard (),
s is Known (Blank number | IRI string) | Wildcard ()
} -> list<{
o is Blank number
| IRI string
| Literal {
language is string,
type is string,
value is string
},
p is IRI string,
s is Blank number | IRI string
}>
> store.match s { s = Wildcard (), p = Wildcard (), o = Wildcard () }
[] is list<{
o is Blank number
| IRI string
| Literal {
language is string,
type is string,
value is string
},
p is IRI string,
s is Blank number | IRI string
}
> store.match s { s = Wildcard (), p = Wildcard (), o = Fruit "banana" }
java.lang.IllegalArgumentException: bad match (Fruit "banana")
at yeti.lang.Core.badMatch(Core.java:216)
at yertle.index$scoreIndexFor.apply(index.yeti:118)
at yertle.index$scoreIndexFor.apply(index.yeti:121)
at yertle.index$scoreIndexFor.apply(index.yeti:121)
at yeti.lang.Fun2_.apply(Unknown Source)
at yeti.lang.Compose.apply(Unknown Source)
at yeti.lang.std$mapIntoHash$.apply(std.yeti:2356)
at yertle.index$chooseIndex.apply(index.yeti:126)
at yertle.store$match.apply(store.yeti:100)
at code.apply(<>:1)
at yeti.lang.compiler.eval._1(eval.yeti:98)
at yeti.lang.compiler.eval.execClass(eval.yeti:76)
at yeti.lang.compiler.eval$evaluateYetiCode$._0(eval.yeti:484)
at yeti.lang.compiler.eval$evaluateYetiCode$.apply(eval.yeti:460)
at yeti.lang.Fun2_.apply(Unknown Source)
at yeti.lang.compiler.yeti.repl(yeti.yeti:59)
at yeti.lang.compiler.yeti.main(yeti.yeti:217)


Chris

[Madis]

On Tue, 19 Feb 2013, Chris Cannam wrote:

> On 22 January 2013 01:41, Madis <ma...@cyber.ee> wrote:
>> I now implemented a bit smarter handling of such case expressions type - it
>> basically still gets extendable variant type, but flagged as also
>> narrowable. Seems like it should work.
>
> At the time I said that this seemed to work -- but I think I may have
> been checking too superficially.
>
>>> f = \case of B (): println "!!!"; _: () esac
>> f is B () -> () = <code$>
>>> g x = (println case x of A x: x; B (): "B" esac; f x);
>> g is A. string | B. () -> () = <code$g>
>>> g is (A. string) -> ()
>> <code$g> is A. string -> ()
>
> But now:
>
>> g (B ())
> B
> !!!
>
> in other words, the compiler reports the narrowed type but still
> accepts the wider type.

I guess the reason here is that g is polymorphic binding - using the
`is' result directly, or rebinding it with the restricted type gives the
binding also the restricted type.

> (g is A. string -> ()) (B ())
1:28: Cannot apply A. string -> () function to B () argument
Type mismatch: A. string => B () (member missing: B)
> g = g is A. string -> ()
g is A. string -> () = <code$g>
> g (B ())
1:7: Cannot apply A. string -> () function (g) to B () argument
Type mismatch: A. string => B () (member missing: B)

> It seems to do this for any function that accepts variant types
> regardless of whether there are any constructed types involved:
>
>> f x is (A number | B number) -> 'a = x
> f is A number | B number -> A number | B number = <code$f>
>> f (C 1)
> C 1 is A number
> | B number
> | C number

This is actually correct - you restricted the type by adding new required
tag C to the required variants set). Had the f x is type been about
accepted types, it would have worked differently:

> f x is (A. number | B. number) -> 'a = x
f is ('a1 is A. number | B. number) -> 'a1 = <code$f>
> f (C 1)
1:6: Cannot apply ('a0 is A. number | B. number) -> 'a0 function (f) to ('a0 is C number) argument
Type mismatch: ('a0 is A. number | B. number) => ('a0 is C number) (member missing: C)

> This can also lead to run-time type errors, for example using the
> default branch of https://bitbucket.org/cannam/yertle:

The above shouldn't.

>> store = load yertle.store
>> s = store.newStore ()
> s is [yertle/store:store]<> = {indexes=[{order=[0,1,2],
> tree=[:]},{order=[1,2,0], tree=[:]},{order=[2,1,0], tree=[:]}]}
>> store.match
> <yertle.store$match> is [yertle/store:store]<> -> {
> o is Known (Blank number
> | IRI string
> | Literal {
> language is string,
> type is string,
> value is string
> }) | Wildcard (),
> p is Known (IRI string) | Wildcard (),
> s is Known (Blank number | IRI string) | Wildcard ()

The argument type seems incorrect - if only Known or Wildcard is
accepted, then those should be in type as Known. or Wildcard. (with dot at
the end). The index module type signature seems correct:
chooseIndex is list<index> -> array<('_g1 is Known. '_e1 | Wildcard. '_f1)> -> index,
match is ('s1 is {`order is list<number>, `tree is ('q0 is hash<'_p1, ('_r1 is Entry` pattern | Sub` 'q0)>)}) -> array<('_u1 is Known. '_p1 | Wildcard. '_t1)> -> list<pattern>,

But store's match is somehow broken - for some reason the following:
match is store -> pattern -> list<statement>.
is incorrectly unified into required (constructed value) tag set in the
Known. _ | Wildcard. _ part, while the result imho actually should be
Known` _ | Wildcard` _ - being both constructed and accepted tags.

[Chris Cannam]

On 19 February 2013 15:19, Madis <ma...@cyber.ee> wrote:
>> f is A number | B number -> A number | B number = <code$f>
>>>
>>> f (C 1)
>>
>> C 1 is A number
>> | B number
>> | C number
>
> This is actually correct - you restricted the type by adding new required
> tag C to the required variants set).

Ah, I get it. That makes sense, though my intuition has been having
difficulties with it.

I think I'd expected it to narrow the accepted variants because (i) it
feels like the way types are narrowed in e.g. "f x is number -> number
= x" and (ii) I can't quite see where the other behaviour would be
useful (?).

>> This can also lead to run-time type errors, for example using the
>> default branch of https://bitbucket.org/cannam/yertle:
>
> The above shouldn't.

Changing the variant typedefs in store.yeti to accepted types gets the
behaviour I had hoped for, so that part is good, thanks.


Chris

[Madis]

On Tue, 19 Feb 2013, Chris Cannam wrote:

> On 19 February 2013 15:19, Madis <ma...@cyber.ee> wrote:
>>> f is A number | B number -> A number | B number = <code$f>
>>>>
>>>> f (C 1)
>>>
>>> C 1 is A number
>>> | B number
>>> | C number
>>
>> This is actually correct - you restricted the type by adding new required
>> tag C to the required variants set).
>
> Ah, I get it. That makes sense, though my intuition has been having
> difficulties with it.
>
> I think I'd expected it to narrow the accepted variants because (i) it
> feels like the way types are narrowed in e.g. "f x is number -> number
> = x" and (ii) I can't quite see where the other behaviour would be
> useful (?).

It's just that the "is" does type unification with the type of expression
on left side - that is - finding the most general type that satisfies both
sides, in other words, the intersection of both types. In the case of
types enumerating all values/properties/cases that the code must be able
to handle it means (maybe counter-intuitively) creating type that includes
all from both types being unified. Maybe the Yeti typesystem exposes it's
internals too directly, but well, that's how it is now.

>>> This can also lead to run-time type errors, for example using the
>>> default branch of https://bitbucket.org/cannam/yertle:
>>
>> The above shouldn't.
>
> Changing the variant typedefs in store.yeti to accepted types gets the
> behaviour I had hoped for, so that part is good, thanks.

Still the resulting type signature shouldn't have been what it was with
old typedefs, so I have to investigate, what went wrong there.

[Chris Cannam]

On 19 February 2013 17:45, Madis <ma...@cyber.ee> wrote:
> Maybe the Yeti typesystem exposes it's internals
> too directly, but well, that's how it is now.

Well, you can't have everything -- there are not many things in Yeti
that you have to remember "just work that way" and I can cope with the
odd one. And at least there is logic to this, it's not entirely a
historical accident.


Chris

[Chris Cannam]

On 19 February 2013 15:19, Madis <ma...@cyber.ee> wrote:

> But store's match is somehow broken - for some reason the following:
> match is store -> pattern -> list<statement>.
> is incorrectly unified

Is the following related, or is it just a consequence of sticking a
structure into a variant into a container without checking its
elements and then pulling it out again in a different context later?

This is with the current tip of the same repo (i.e. now using the
dot-suffixed constructed variant types), not with the rev ba09124df7b0
that I referred to previously.

> store = load yertle.store
store is [..elided..]
> st = store.newStore ()
st is [..elided..]
> store.add
<yertle.store$add> is [yertle/store:store]<> -> {
o is Blank. number
| IRI. string
| Literal. {

language is string,
type is string,
value is string

},
p is IRI. string,
s is Blank. number | IRI. string
} -> boolean
> store.add st { s = IRI "a", p = IRI "b", o = Literal { value = "pie" } }
true is boolean
> store.enumerate st
[{o=Literal {value="pie"}, p=IRI "b", s=IRI "a"}] is list<{
o is Blank. number
| IRI. string
| Literal. {

language is string,
type is string,
value is string

},
p is IRI. string,
s is Blank. number | IRI. string
}>
> node = (head (store.enumerate st)).o
node is Blank. number
| IRI. string
| Literal. {

language is string,
type is string,
value is string

} = Literal {value="pie"}
> case node of Literal lit: lit.value esac
"pie" is string
> case node of Literal lit: lit.type esac
java.lang.ArrayIndexOutOfBoundsException: 1
at yeti.lang.Struct3.get(Struct3.java:48)

at code.apply(<>:1)
at yeti.lang.compiler.eval._1(eval.yeti:98)
at yeti.lang.compiler.eval.execClass(eval.yeti:76)
at yeti.lang.compiler.eval$evaluateYetiCode$._0(eval.yeti:484)
at yeti.lang.compiler.eval$evaluateYetiCode$.apply(eval.yeti:460)
at yeti.lang.Fun2_.apply(Unknown Source)
at yeti.lang.compiler.yeti.repl(yeti.yeti:59)
at yeti.lang.compiler.yeti.main(yeti.yeti:217)

> case node of Blank b: b esac
java.lang.IllegalArgumentException: bad match (Literal {value="pie"})
at yeti.lang.Core.badMatch(Core.java:216)
at code.apply(<>)

[Madis]

On Wed, 20 Feb 2013, Chris Cannam wrote:

> On 19 February 2013 15:19, Madis <ma...@cyber.ee> wrote:
>> But store's match is somehow broken - for some reason the following:
>> match is store -> pattern -> list<statement>.
>> is incorrectly unified
>
> Is the following related, or is it just a consequence of sticking a
> structure into a variant into a container without checking its
> elements and then pulling it out again in a different context later?

I think that the cause is exactly the same as was with variants:

> | Literal. {
> language is string,
> type is string,
> value is string
> },
> p is IRI. string,
> s is Blank. number | IRI. string
> } -> boolean

Should be:
| Literal. {
.language is string,
.type is string,
.value is string
},

The simple rule is that, when the type denotes value that is to be
consumed (like function argument), then it should have the dot's. If it's
denoting value produced (like function return type), then it shouldn't
have the dots.

As said before, I have to look why it gets the unification wrong there
(it looks a bit like it's discarding the original inferred type for some
unknown reason).

Additionally I have idea, how to make typedefs a bit easier to use in this
regard (I think it is probably possible to get a default behaviour where
typedef struct/variant automatically chooses whether it's defining
accepted or required fields/variants when the typedef is used). But these
are separate issues - first is clear bug in current implementation, and
second a feature that would be nice to have.

[Chris Cannam]

On 20 February 2013 19:00, Madis <ma...@cyber.ee> wrote:
>
> The simple rule is that, when the type denotes value that is to be consumed
> (like function argument), then it should have the dot's. If it's denoting
> value produced (like function return type), then it shouldn't have the dots.

> [...]

> Additionally I have idea, how to make typedefs a bit easier to use in this
> regard (I think it is probably possible to get a default behaviour where
> typedef struct/variant automatically chooses whether it's defining accepted
> or required fields/variants when the typedef is used).

I see... What are the consequences, as of now, of using the same
typedef containing constructed types on both sides, i.e. as return
value as well? That is, having a single e.g. typedef statement = { .s
is IRI. string | Blank. number, .p is IRI string (etc) } and using it
everywhere a statement is either accepted by or returned from a
function?

[I'm seeing no bad consequences at the moment, but it troubles me a
bit that the original version (without constructed types) also worked
fine for as long as the code that was using it was correct, but then
blew up in a rather de-localised way when a module passed in the wrong
type. It would be nice to be certain that the apparent type contract
of a function wasn't being undermined silently by accidental elisions
or typos.]


Chris

[Madis]

On Wed, 20 Feb 2013, Chris Cannam wrote:

Without the unification bug I mentioned before, the result of using
the old typedef variant would have been just overly strict type
signature, potentially disallowing some code that would work otherwise.
The bug probably gets fixed in a week or so, I just have too many other
things to do at the moment.

[chrisichris]

The simple rule is that, when the type denotes value that is to be
consumed (like function argument), then it should have the dot's. If it's
denoting value produced (like function return type), then it shouldn't
have the dots.

Just a stupid theoritical question: does a variant type which has both a consumed (dotted, accepted) and a produced (undotted, constructed) variant make sense:

> f x is (A. number | B number) -> 'a = x

f is A. number | B number -> A. number | B number = <code$f>

> f (A 1)

A 1 is A` number | B number

> f (B 1)

1:6: Cannot apply A. number | B number -> A. number | B number function (f) to B number argument

    Type mismatch: A. number | B number => B number (member missing: B)

if not - because all Variants have to be either accepted or produced - maybe the accepted variant type should be presented in squar-brackets

f x is [A number | B number] -> 'a === f x is (A. number | B. number) -> 'a

 

[Madis]

On Thu, 21 Feb 2013, chrisichris wrote:

>
> The simple rule is that, when the type denotes value that is to be
> consumed (like function argument), then it should have the dot's. If it's
> denoting value produced (like function return type), then it shouldn't
> have the dots.
>
>
> Just a stupid theoritical question: does a variant type which has both a consumed (dotted,
> accepted) and a produced (undotted, constructed) variant make sense:
>
> > f x is (A. number | B number) -> 'a = x
> f is A. number | B number -> A. number | B number = <code$f>

Actually these shouldn't be mixed (known problem - probably should give
compiler error here). But there is case where ` should be mixed with .:

> f x = case x of A _: x; B _: x esac
f is ('c is A. 'a | B. 'b) -> 'c = <code$f>
> f (A 1)
A 1 is A` number | B. 'a
^--- and ---^

> f x is [A number | B number] -> 'a === f x is (A. number | B. number) -> 'a

What about structures? They have exactly the same semantics in reverse.

[chrisichris]

For accepted structs a double {{  alternatively {. (and (. for variants)? IMO square brackets and double brackets are easier to read.

Apart of that 

When trying creating a structure with consumed and produced memember I used - my favorite - with.

> fn x = x with {c = x.a + x.b}

fn is {

   .a is number,

   .b is number,

   .c is number

} -> {

   .a is number,

   .b is number,

   .c is number

} = <code$fn>

> fn {a = 2, b=3}

1:4: Cannot apply { ....

This is obvioulsy not what you want.

However when doing explicit type declarations: I get a' types, which is nice:

> fn x is {a is number, b is number} -> 'c = x with {c = x.a + x.b}

fn is {`a is number, `b is number} -> {

   a is number,

   b is number,

   c is number

} = <code$fn>

Could the compiler do that (some time in the future) without type delcaration?

Maybe (in the even further future) a second form of 'with' would be useful which demands that all memebers of left are accepted of ones on the right: 

My use case is when doing configurations (ie in ybuilder) I use structures composed with "with". Customizing the configuration than should happen by overwriding certain values ie:

ie if I have differnte parts to compose a (build system) with defaultConfigs for the parts:

defaultConfigA = {a_name = .., , a_y = ..};

defaultConfigB = {b_id = ..., b_y =..} ;

partA conf is {a_name is, a_y ..} -> 'a = conf with {a_calculated = };

partB conf is {b_id is ..., a_calculated = ..} -> 'a = conf with {b_calc = a_calculated ^ b_id}; 

than I use them to compose a build-system:

conf = defaultConfigA with defaulConfigB 

          with //customize 

          {a_name = "foo"};

runSystem  (partB . partA) conf;

The problem here is that the customize "with" is not typechecked because I could also misspell {a_nam = "foo"} and the compiler would accept it. So maybe two types of with one strict where the lefttype must have all fields accepted which are on the right. And the "normal" with which is just a producing with. (However this is no necessity the pattern can still be used because I use currently vars for custimizaiton)

[Chris Cannam]

On 21 February 2013 08:46, chrisichris <christ...@googlemail.com> wrote:
> Just a stupid theoritical question: does a variant type which has both a
> consumed (dotted, accepted) and a produced (undotted, constructed) variant
> make sense:

Haha, glad you asked that one -- I'd been thinking the same question,
but reckoned I'd used up my quota for the day...


Chris

[Madis]

On Tue, 19 Feb 2013, Chris Cannam wrote:

>> store = load yertle.store
>> s = store.newStore ()
> s is [yertle/store:store]<> = {indexes=[{order=[0,1,2],
> tree=[:]},{order=[1,2,0], tree=[:]},{order=[2,1,0], tree=[:]}]}
>> store.match
> <yertle.store$match> is [yertle/store:store]<> -> {
> o is Known (Blank number
> | IRI string
> | Literal {
> language is string,
> type is string,
> value is string
> }) | Wildcard (),
> p is Known (IRI string) | Wildcard (),
> s is Known (Blank number | IRI string) | Wildcard ()

Looked into it, it's problem with as cast implementation when used for
casts between Yeti types (opaque type cast). Should be possible to fix,
I'll try it sometime. It shouldn't affect any Yeti code not using as cast
in this way (as cast to/from Java types is ok).

[Madis]

I hope it's fixed now (in git and the git build).

[Chris Cannam]

On 9 March 2013 12:29, Madis <ma...@cyber.ee> wrote:
> I hope it's fixed now (in git and the git build).

Hm, now my variant alternations have only one variant in them in their
reported types.

In current git (revisions from f2a7299 onwards) of yeti, with the
current head of my yertle code, the yertle.store module is reported as
having type

{
newRdfStore = <yertle.store$newRdfStore>
} is {newRdfStore is () -> {
abbreviate is IRI` string -> string,
add is {
.o is IRI. string,
.p is IRI. string,
.s is IRI. string
} -> (),

etc, where every variant alternation has IRI type only. Prior to that
commit in yeti, with the same yertle code, the module type was

{
newRdfStore = <yertle.store$newRdfStore>
} is {newRdfStore is () -> {
abbreviate is IRI string -> string,
add is {
.o is Blank. number
| IRI. string

| Literal. {
.language is string,
.type is string,
.value is string
},

.p is IRI. string,
.s is Blank. number | IRI. string
} -> (),

etc, which is what I'd expected to see. Code calling this module
correspondingly fails to compile. Something broken, or exposing an
existing misconception on my part?


Chris

[Madis]

On Sat, 9 Mar 2013, Chris Cannam wrote:

> On 9 March 2013 12:29, Madis <ma...@cyber.ee> wrote:
>> I hope it's fixed now (in git and the git build).
>
> Hm, now my variant alternations have only one variant in them in their
> reported types.

It's not so with the february version of yertle.
With current version, you can see the reason when you remove the as cast
and look the derived module signature without it:

newRdfStore is () -> {
abbreviate is iri -> string,
add is {
.o is '_a,
.p is '_a,
.s is '_a
} -> (),
addPrefix is string -> string -> (),
contains is {
.o is '_a,
.p is '_a,
.s is '_a
} -> boolean,
enumerate is () -> list<{
.o is '_a,
.p is '_a,
.s is '_a
}>,
expand is string -> iri,
havePrefix is string -> boolean,
match is {
.o is ('c is Known. '_a | Wildcard. '_b),
.p is 'c,
.s is 'c
} -> list<{
.o is '_a,
.p is '_a,
.s is '_a
}>,
prefixes is () -> list<string>,
remove is {
.o is '_a,
.p is '_a,
.s is '_a
} -> boolean
}

All the structure field types in your given signature get unified with '_a
in this signature, meaning all get also unified with triples .p type (IRI.
string). As this is the most restrictive type there, it is the resulting
type for all those fields. I guess the reason is processing all the fields
with map, joining the types into single '_a. It's simply not possible for
as cast to safely derive the desired module type signature from this
inferred type, so I'm afraid that you have to change your code.

Previously as cast didn't adjust the result type to the inferred one,
that's why it seemed to work here, and that's also why it resulted in
signature that allowed a code using it to crash.

[Chris Cannam]

On 9 March 2013 16:43, Madis <ma...@cyber.ee> wrote:
> As this is the most restrictive type there, it is the resulting
> type for all those fields. I guess the reason is processing all the fields
> with map, joining the types into single '_a. It's simply not possible for as
> cast to safely derive the desired module type signature from this inferred
> type, so I'm afraid that you have to change your code.

OK, that makes sense and seems simpler than the previous behaviour.
I'll take another angle for this code and see how I get on.

Thanks,


Chris