Rule out messages with abstract types in the type checker

[nomeata]

My work-in-progress implementation of type-based serialization
asserts false when it encounters such, but it is much nicer to just
rule them out statically.

I updated some tests that were using abstract types in messages, but
were (I believe) testing something else to use concrete types.

[crusso]

Should you not check the bounds are concrete or at least empty too?

[nomeata]

Right … I do that on terms, so I should do it on types..

Initially I thought I only check for occurrences, i.e. allow a shared function to be polymorphic as long as the type was not used, which would be fine, but useless and possibly confusing.

[crusso]

Unless you only use this on opened types, you may want to return false in the Var _ case, no?

[nomeata]

Ah, right, that part of probably not right yet. I thought I can work on types without opening, but that would allow hiding a non-concrete type somewhere inside. Will have to come up with a test case and revise.

I fact, why does it even complain about

{ let x : ?(<A <: Shared>(shared A -> ()) -> ()) = null; };

then?

Well, tomorrow…

[crusso]

but see comments - we can always improve later so I'm happy to merge as is.

[nomeata]

This is actually broken in a few ways. Will give it a fresh start tomorrow.

[rossberg]

I'm not sure I understand the criterion. Shouldn't e.g.

func f<A <: Shared>(x : shared A -> ()) = ...

be allowed?

[crusso]

I don't see how you can allow that if you do static serialization but don't monomorphise or pass types. Get Outlook for Android<https://aka.ms/ghei36>

…

________________________________ From: Andreas Rossberg <notifications@github.com> Sent: Tuesday, March 19, 2019 6:50:06 AM To: dfinity-lab/actorscript Cc: Claudio Russo; Review requested Subject: Re: [dfinity-lab/actorscript] Rule out messages with abstract types in the type checker (#247) I'm not sure I understand the criterion. Shouldn't e.g. func f<A <: Shared>(x : shared A -> ()) = ... be allowed? — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub<#247 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AAFPHDYgn1DBE4Xpk_306lywUWnKvgYqks5vYIiegaJpZM4b6T1h>.

[crusso]

Oh, maybe you can allow this, provided you rule out the *introduction* of any shared function with type parameters or open type and the function not the caller does the serialization Get Outlook for Android<https://aka.ms/ghei36>

…

________________________________ From: Claudio Russo <notifications@github.com> Sent: Tuesday, March 19, 2019 7:23:45 AM To: dfinity-lab/actorscript Cc: Claudio Russo; Your activity Subject: Re: [dfinity-lab/actorscript] Rule out messages with abstract types in the type checker (#247) I don't see how you can allow that if you do static serialization but don't monomorphise or pass types. Get Outlook for Android<https://aka.ms/ghei36>

________________________________ From: Andreas Rossberg <notifications@github.com> Sent: Tuesday, March 19, 2019 6:50:06 AM To: dfinity-lab/actorscript Cc: Claudio Russo; Review requested Subject: Re: [dfinity-lab/actorscript] Rule out messages with abstract types in the type checker (#247) I'm not sure I understand the criterion. Shouldn't e.g. func f<A <: Shared>(x : shared A -> ()) = ... be allowed? — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub<#247 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AAFPHDYgn1DBE4Xpk_306lywUWnKvgYqks5vYIiegaJpZM4b6T1h>. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub<#247 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/AAFPHIQ9Z9rJJ1dO_7pKL5uV1AGuZn5Xks5vYJCBgaJpZM4b6T1h>.

[nomeata]

I have a new criterion in mind, which works better with type aliases that use parameters in shared function arguments, will work on it in the afternoon.

But here is a peek preview. It would actually

func f<A <: Shared>(x : shared A -> ()) : (shared A -> ()) = x

could actually allowed (f never has to serialize or deserialize a value of type A), and we can call f<Int>(g) or f<Bool>(h) without problem. Just not f<B>(g) where B is an abstract type.

The idea is, for a type t find it’s relevant free type constructors, written as c relevant t for “c is relevant in t”. The idea is that c relevant t if we need to know c to know the representation of t as a message. The rules could be

1. c relevant c if kind c = Abs _
2. c relevant c[t] if kind c = Def (λd. t2) if d relevant t2 and and c relevant t (we look through type definitions)
3. c relevant ?t if c relevant t (and similar for tuples, lists, local objects)
4. We can actually soundly have no rules functions and actors, because we do not need to know their arguments (resp. fields) to know their representation. (This is just a neat observation, and may no longer be true if we want to generate an IDL signature for our actors when the IDL language does not support abstract types. So I guess we should just look through functions and actors as well)

Then the rule for FuncE and CallE is that for all argument and return types t, if c relevant t, then this is an error (and we can helpfully report which c there is).

Note that we don't have to normalize c[t] in 2. and we only have to analyze the right-hand side of c once, so this can be implemented even for non-uniform recursive types not true actually. (That part reminds me of the work on Roles in Haskell, my most cited paper :-))

[nomeata]

New version at #250 (less ambitious than the analysis outlined here).