questions on the type system

[Răzvan Rotaru]

Hi,

I'm currently playing around with yeti, trying to understand the type system, and I have two questions:

1/

> myfun a b = if a==b then {a=15} else "blabla" fi
1:38: This if branch has a string type, while another was a {a is number}

So the code above is not allowed by the type system. Is there a particular reason for that? Is it difficult to implement? I have seen something like this being supported in julia with what they call type unions. It's true that julia doesn't do static typing, but I find the idea quite useful.

2/

> myfun a b = if a==b then {x=15} else {x=15, y=20} fi
myfun is 'a -> 'a -> {x is number} = <code$myfun>
> myfun 10 20
{x=15, y=20} is {x is number}
> myfun 10 10
{x=15} is {x is number}

Let me first say that I find the duck-typing-like behaviours of structure to be brilliant. A lot of Java code does nothing more than coerce a class to another, and I think that yeti structures don't suffer from that.

In the code above "y" does not seem to exist in the type of myfun, and also in the result "{x=15, y=20}". This does not look right to me. Why is "y" ignored by the type system?


Cheers,
Răzvan

[chrisichris]

On Tuesday, January 6, 2015 9:25:42 PM UTC+1, Răzvan Rotaru wrote:

Hi,

I'm currently playing around with yeti, trying to understand the type system, and I have two questions:

1/

> myfun a b = if a==b then {a=15} else "blabla" fi
1:38: This if branch has a string type, while another was a {a is number}

So the code above is not allowed by the type system. Is there a particular reason for that? Is it difficult to implement? I have seen something like this being supported in julia with what they call type unions. It's true that julia doesn't do static typing, but I find the idea quite useful.

Union types are implemented as variant tags (the types with the upper-case letter).

> myFn a b = if a == b then Left {a=10} else BlaStr "blabla" fi
myFn is 'a -> 'a -> BlaStr string | Left {a is number} = <code$myFn>

see http://dot.planet.ee/yeti/intro.html#variant-types

 

2/

> myfun a b = if a==b then {x=15} else {x=15, y=20} fi
myfun is 'a -> 'a -> {x is number} = <code$myfun>
> myfun 10 20
{x=15, y=20} is {x is number}
> myfun 10 10
{x=15} is {x is number}

Let me first say that I find the duck-typing-like behaviours of structure to be brilliant. A lot of Java code does nothing more than coerce a class to another, and I think that yeti structures don't suffer from that.

In the code above "y" does not seem to exist in the type of myfun, and also in the result "{x=15, y=20}". This does not look right to me. Why is "y" ignored by the type system?

The return-type of the function is {x is number} and this type does not change no matter which value you pass as parameter.  because at compile time the compiler does not know wheter you pass two different params or equal ones.

What you see in the repl output is the runtime value first and after the 'is' the type. While the runtime-value is indeed different the type is always the same

 

Cheers,
Răzvan

[ma...@cyber.ee]

On Tue, 6 Jan 2015, Răzvan Rotaru wrote:

> I'm currently playing around with yeti, trying to understand the type
> system, and I have two questions:
>
> 1/
>> myfun a b = if a==b then {a=15} else "blabla" fi
> 1:38: This if branch has a string type, while another was a {a is number}
>
> So the code above is not allowed by the type system. Is there a particular
> reason for that? Is it difficult to implement? I have seen something like

> this being supported in julia <http://julialang.org/> with what they call type
> unions <http://docs.julialang.org/en/release-0.3/manual/types/#type-unions>.

> It's true that julia doesn't do static typing, but I find the idea quite
> useful.

Yeti implements ML type system with some extensions (like extensible
record and variant types), being most similar to the OCaml type system.
Direct union types are not supported, but you can use variant types
(which are also called tagged unions) to return values of different types.

> myfun a b = if a==b then X {a=15} else Y "blabla" fi
myfun is 'a -> 'a -> X {a is number} | Y string = <code$myfun>
> test = \case of X {a}: println "got \(a)"; Y s: println s esac
test is X. {.a is 'a} | Y. 'b -> () = <code$>
> test (myfun 1 1)
got 15
> test (myfun 1 2)
blabla

>> myfun a b = if a==b then {x=15} else {x=15, y=20} fi
> myfun is 'a -> 'a -> {x is number} = <code$myfun>
>> myfun 10 20
> {x=15, y=20} is {x is number}
>> myfun 10 10
> {x=15} is {x is number}
>
> Let me first say that I find the duck-typing-like behaviours of structure
> to be brilliant. A lot of Java code does nothing more than coerce a class
> to another, and I think that yeti structures don't suffer from that.
> In the code above "y" does not seem to exist in the type of myfun, and also
> in the result "{x=15, y=20}". This does not look right to me. Why is "y"
> ignored by the type system?

Because expression can have only one type and the if-else infers basically
the common subset of the branches structure types, to guarantee that all
operations possible with this type would be possible with all values that
can arise from the if-else expression.

While the REPL shows both fields in the value, you can only access x in
this case, as the compiler knows that only that field is always present
in the returned value.

Basically the mission of the type checker is to disallow anything that
could implicitly fail at runtime. It isn't totally thorough in this - for
example it doesn't care about exceptions that might be thrown by
functions, it allows all Java values to be nullable (and therefore
accessing those can result in NullPointerException), and all bets will be
off when you (mis)use unsafely_as casts. But using the core language
operations like structure field access shouldn't result in runtime errors
unless something catastrophic has happened.

[chrisichris]

Is there a particular (technical) reason why direct union types are not supported ?

[Răzvan Rotaru]

Here's another interesting situation:

> myfun x = case x of {a = va}: va; {a = va, b = vb}: va+vb; esac;
myfun is {.a is number, .b is number} -> number = <code$myfun>
> myfun {a=10}
1:7: Cannot apply {.a is number, .b is number} -> number function (myfun) to {a is number} argument
    Type mismatch: {a is number} => {.a is number, .b is number} (member missing: b)

So here the type of myfun is a structure containing all fields, not only the common ones, like when using "if". Is this the intended behaviour? This looks inconsistent to me.

Furthermore, there seems to be a bug here:

> myfun {a=10,b=20}
10 is number

(according to the definition above, the result should be 30, not 10).

Cheers,
Răzvan

[Madis]

No bug, although the compiler could warn that the second case is
unreachable, because the first one matches always.

The deduced type is also technically correct, because if the second case
were reached then the b field would be used.

You seem to be misunderstanding what the case ... esac matches - it
doesn't look at the type at all, the types are checked at compile time.
The case expression looks only at values. With variant and structure types
there is single type assigned for every expression in the program at
compile time. The type can be polymorphic, but it's still a single type,
that for variant and structure types describes all the variants and
fields that are relevant at this place in the code.

With variant types the runtime value has tag that can be matched, but with
structure types _all_ the fields known must be present at runtime, and no
decisions can be done based on the existance of fields therefore. The
fact that you are allowed to call polymorphic function with structure
having more fields as argument, is not relevant inside that function.

If you want to give different structures, then you must use variant types.