Question: type assertion / typeof

[Mehgugs]

I'd just like to preface this by saying thank you for the excellent blog on implementing cubiml, and I hope I'm not necro-ing a project with questions.

With that said, I've finished your tutorial and added a couple of minor extensions. Would a form of type assertion be possible in this system (similar to how null is disambiguated)?:

if <expr> is <type> then etc..

EDIT:

For clarification the point of this would be to unpick a union for example.

[Storyyeller]

Isn't that just another form of match expression?

[Mehgugs]

Yes, that is essentially it. So for a match arm with a type sig (maybe it looks like (x : Int) -> .... or something) do I just flow the two results of parse_type into the wrapped type var? Perhaps I was overthinking this.

EDIT: Maybe the parse_type simply replaces the type var altogether in that branch now that I think about it more?

Sorry for rubber ducking a bit here... But the part at which the type heads are checked is what is really eluding me.

So I've got some use type which contains an array of all the arm sigs respectively. Now when we "check heads" we want to say if the lhs matches one of these branches it's fine. For the variant only match this is easy, we look up the tag in the case use and flow the lhs to the corresponding use value (and also force the lazy flow). For a more general match pattern, how do we do something analogous to "look up the tag"?

[Storyyeller]

I think you would just treat it as multiple nested matches, with all the else branches going to the same place.

Depending on what exactly you want to match on, you may need to redesign your type system in order to allow matching. The type system presented in CubiML only allows matching on null and on sum type tags, but you can easily modify it to match on say str, int, etc. if you want to.

[Mehgugs]

for context I have added top level type aliases which means it's easy to label a complex type definition that you want to reuse.

My pipe dream is a match that can support the following:

type IntList = {val : int; next: Self}? -- these top level aliases have Self recursively bound for ease of construction

match something with 
  | (x : IntList) -> some_expr
  | (y : int) -> and_so_on

But I feel like that may be hard to do.

Would a use type which stores a typehead and then "the next typehead" in a linked list style be able to handle this kind of construct?

If you check the head and if it fails you would push a constraint of ind_lhs and the "tail" of the use type which would prompt it to try the next one in the chain? I suppose the issue is that you cannot primitively match (VSomething, USomething) for all types.

[Storyyeller]

Matching against a recursive type like that would require a potentially infinite number of runtime checks, so I don't think that is a good idea.

[Mehgugs]

Yeah, I was thinking more on it and I think something that can match primitive types like int and str would be sufficient for most real usages. I also realized that the whole point of variants is to discriminate on complex types anyway, so why not just define a variant or even use nullables.

I do have another smaller question which is somewhat unrelated and more of an opinion. I've noticed that in this type system you can construct definitions like:

let x = (1 : number)

Do you think these should be rejected at compile time (if we try to type a literal with a superposition) or are there legit reasons people might want to do this? Can we "ignore" this type declaration if that is the case.

[Storyyeller]

For a simple didactic language, of course simplicity always wins. If you're considering a more complex "real world" language, it's a tradeoff. You have to choose between the benefits of simplicity and consistency versus the benefits of adding arbitrary restrictions in order to rule out confusing or likely erroneous code patterns. I personally don't see how this qualifies as that though.

[Mehgugs]

Well this case is a bit special but, as a more general example, you can effectively limit usages by typing anything as top, even literals. I was asking if you could think of any programs where using this is a benefit out of curiosity. For example, I think a value that is constrained to top would function like some kind of sentinel/ID which you never want consumers to do operations on except equality right? Perhaps this has an analogue in a more conventional system?

[Mehgugs]

I'm gonna close this, the upshot is:

• I expanded case_use and match expressions to also match on primitives, and allowed case type signatures to contain those primitives.
• This obsoletes null handling since you can just match on Null -> now.
• Looking at adding something like newtype to box primitive types in the future.