Stream: beginners

Topic: Abilities with type variables

Kilian Vounckx (Jul 06 2023 at 13:25):

Is it posible to make abilities with type variables?

I was playing around with roc and wanted to make an Iterator (similar to the rust trait) to see how it would work. I tried the following but it doesn't parse:

Iterator item has
    next : iter -> Result (item, iter) | iter has Iterator

If I try it without the type variable, it does parse:

Iterator has
    next : iter -> Result (item, iter) | iter has Iterator

I'm not yet sure if the type variable is needed, so I will keep playing around. I am mainly checking if this is a bug, a planned unimplemented feature, or not planned at all

Ayaz Hafiz (Jul 06 2023 at 14:00):

It's not planned. The current design is that an ability can only specialize over the type the ability is implemented for, and no other type variable.

You can however support unbound polymorphic variables in the member signatures, for example something like

WeirdId has
  id : a, me -> a | me has WeirdId

and an impl like

Foo := {} has [WeirdId.{id}]
id = \anything, @Foo {} -> anything

is allowed

Kilian Vounckx (Jul 06 2023 at 14:38):

I see, thanks for the answer.

Is there a specific reason for this choice? Like performance, ease of implementation, ...

Ayaz Hafiz (Jul 06 2023 at 14:42):

The main one is the scope of abilities - we would like to reduce the scope of ad-hoc polymorphism as much as possible for now, until such a time as we see necessary demand for any larger scope. Our current hypothesis is that in practice the scope will not need to be larger than it is now (that is, no need for ad-hoc polymorphism over more than one type variable).
It is a nice coincidence that the compiler performance is much better when you have only one type variable to resolve over, but that is secondary reason to the scope of the feature.

Kilian Vounckx (Jul 06 2023 at 14:51):

Okay makes sense.
I was surprised to see the following work though

ability Iter has
    next : iter -> Result (iter, item) [IterDone] | iter has Iter

Map iter a b := {
    base : iter,
    func : a -> b,
} has
    [
        Iter { next: nextMap },
    ]

nextMap : Map iter a b -> Result (Map iter a b, b) [IterDone] | iter has Iter
nextMap = \@Map { base, func } ->
    when next base is
        Ok (newBase, item) -> Ok (@Map { base: newBase, func }, func item)
        Err IterDone -> Err IterDone

map : iter, (a -> b) -> Map iter a b | iter has Iter
map = \iter, func -> @Map {
    base: iter,
    func,
}

I know this doesn't seem like idiomatic roc at all (as far as idiomatic roc exists), but it was a proof of concept. What I found surprising was that in the nextMap function we never have to specify that the iterator items are the same as the map's function input variable.

Nowhere in the signature of map does it show this, yet it still works

Ayaz Hafiz (Jul 06 2023 at 15:13):

It works because item in the return type of the next member is unbound in the input arguments, and so can be instantiated to any type (in this case, the a of the Map constructor). But that also means that you could not implement Iter for a ground type (that is, one that does not contain a nested iter | iter has Iter value), without only returning the Err variant for Iter#next.

Ayaz Hafiz (Jul 06 2023 at 15:14):

Iter#next is effectively asking for the equivalent of a function iter -> item, where item has no relation to iter, and therefore must be able to be instantiated to any type. No such value exists.

Kilian Vounckx (Jul 06 2023 at 15:17):

Ayaz Hafiz said:

It works because item in the return type of the next member is unbound in the input arguments, and so can be instantiated to any type (in this case, the a of the Map constructor). But that also means that you could not implement Iter for a ground type (that is, one that does not contain a nested iter | iter has Iter value), without only returning the Err variant for Iter#next.

What do you mean by ground type exactly? I have an iterator which iterates over lists:

ListIter a := {
    list : List a,
    index : Nat,
}
     has [
         Iter { next: nextList },
     ]

nextList : ListIter item -> Result (ListIter item, item) [IterDone]
nextList = \@ListIter { list, index } ->
    when List.get list index is
        Ok item -> Ok (@ListIter { list, index: index + 1 }, item)
        Err OutOfBounds -> Err IterDo

It does not contain a nested iter, yet still works

Ayaz Hafiz (Jul 06 2023 at 15:20):

could you share your whole program in a GitHub gist or something similar?

Ayaz Hafiz (Jul 06 2023 at 15:20):

maybe you have found a soundness hole :nerd:

Kilian Vounckx (Jul 06 2023 at 15:24):

https://gist.github.com/KilianVounckx/227dca42606a5eafc7f3fa6e2482b045

Kilian Vounckx (Jul 06 2023 at 15:24):

I can make a smaller one without the iterator adaptors I already made if that would be clearer

Kilian Vounckx (Jul 06 2023 at 15:26):

I added a more minimal one with only the list iterator and toList function

Ayaz Hafiz (Jul 06 2023 at 15:26):

thanks! will take a look soon

Ayaz Hafiz (Jul 06 2023 at 17:25):

Nice. Yeah this is definitely a soundness hole

Ayaz Hafiz (Jul 06 2023 at 17:26):

You'll notice that in theory, it should also be possible to write

expect
    toList (intoIter (iterList [1, 2, 3])) == ["1", "2", "3"]

this doesn't work, the compiler blows up, but it should catch this whole program as incorrect

Ayaz Hafiz (Jul 06 2023 at 17:28):

The problem is that this type signature

nextList : ListIter item -> Result (ListIter item, item) [IterDone]

does not line up with

    next : iter -> Result (iter, item) [IterDone] | iter has Iter

in the item position, in that the compiler lets you instantiate it as a concrete type related to ListIter item, when it should not

Ayaz Hafiz (Jul 06 2023 at 18:37):

I filed https://github.com/roc-lang/roc/issues/5645 and raised what is needed to address this soundness bug in #compiler development (public) > Sound type-checking of ability implementations. Thanks again for catching this!

Last updated: Jul 05 2025 at 12:14 UTC