Stream: compiler development

Topic: Higher Kinded?

Brendan Hansknecht (Aug 28 2024 at 04:37):

From the iterator discussion, I am questioning if certain features we are taking advantage of are meant to work in Roc or if they accidentally happened to work? Also, if they accidentally happened to work, do we actually want them to work?

Fundamentally, this is around higher kinded types and abilities. I feel like some of what works today is equivalent to using higher kinded types but with a worse api that fails to track the higher kinded relationships.

As the most simple example:

SequenceWalker seq state elem : seq, state, (state, elem -> state) -> state

This sequence walker type really should be a higher kinded realationship. It should be a sequence of elem type. Instead we have a fully opaque sequence. We then introduce an elem type that is not anchored to anything in the expression. To me, this strictly feels like failing to fully map out the relationship between seq and elem. This has the same features as a higher kinded type would give without any of the type information. Do we gain anything from banning higher kinded types here?

This second example is a continution with something that works as a iterable:

Walker state elem : state, (state, elem -> state) -> state

Iterable implements
    createWalkFn : iter -> Walker state elem where iter implements Iterable

This Iterable api works. That said, it is clearly lacking information. We have no indication that the iterator is over the correct element type. Roc will still end up properly specializing and type checking this code, but it fundamentally feels wrong to me.

I guess my questions are really two fold:

1. Is this something that we intentionally want to work? My gut feeling is that it is a fluke that this work and we really should be getting some sort of complaint about generalization and the usage of an unknown elem type variable. Cause this api suggest that and Iterable should be able to walk over any element type. This is obviously not correct. An iterable can only walk over the specific element type that it is generating. A List Int and can support a Str walking function, but this api suggest that is valid.
2. If this should work, why don't we support higher kinded types? To me, this feels like higher kinded types but with a worse api.

Brendan Hansknecht (Aug 28 2024 at 04:39):

Something just rings wrong to me here. There is a relationship between the sequence/iterator and the element type, but it is not represented in these apis despite definitely mattering.

Brendan Hansknecht (Aug 28 2024 at 04:49):

Yeah, I think I see the error I would expect. Looking at SequenceWalker vs List.walk:

SequenceWalker seq state elem : seq, state, (state, elem -> state) -> state

List.walk : List elem, state, (state, elem -> state)-> state

I think there should be an error that say the function List.walk is not general enough to satisfy SequenceWalker. SequenceWalker requires a function seq, state, (state, elem -> state) -> state where there is no relationship between seq and elem. List.walk requires a relationship between seq (which is List elem) and elem (which is still elem). So List.walk is not general enough to be a SequenceWalker.

Not saying this is a useful error to produce. It may be better that we allow this kind of relationship. But I do think it is a form of allowing higher kinded types while hiding them from the type system.

Brendan Hansknecht (Aug 28 2024 at 05:35):

For reference, I just took two examples of monads from https://blog.oliverbalfour.com/haskell/2020/08/08/understanding-monads-haskell.html and implemented them in Roc.

To my understanding, this shouldn't be possible in Roc, but it works today.

app [main] { pf: platform "https://github.com/roc-lang/basic-cli/releases/download/0.14.0/dC5ceT962N_4jmoyoffVdphJ_4GlW3YMhAPyGPr-nU0.tar.br" }

import pf.Stdout
import pf.Task exposing [Task]

Monad implements
    bind : ma, (a -> mb) -> mb where ma implements Monad
    return : a -> ma where ma implements Monad

# Note: I expected to need this ability and to apply it to `mb` above, but it turns out that it isn't even required
# ToMonad implements
#     toMonad : ma -> ma where ma implements ToMonad & Monad


Option a := [Some a, None] implements [
        Monad {
            bind: bindOption,
            return: returnOption,
        },
    ]

bindOption = \@Option option, map ->
    when option is
        Some a ->
            map a

        None ->
            @Option None

returnOption = \a ->
    @Option (Some a)

MonadicList a := List a implements [
        Monad {
            bind: bindList,
            return: returnList,
        },
    ]

bindList = \@MonadicList l, map ->
    List.walk l [] \accum, elem ->
        (@MonadicList new) = map elem
        List.concat accum new
    |> @MonadicList

returnList = \a -> @MonadicList [a]

brownian = \n ->
    @MonadicList [n - 1, n + 1]

main =
    x : Option I64
    x = return 27

    y = bind x \v -> @Option (Some (Num.toStr v))

    z = bind y \str -> @Option (Some (Str.concat str " is a value in a monad"))

    brownian 0
        |> bind brownian
        |> bind brownian
        |> \@MonadicList l -> l
        |> Inspect.toStr
        |> Stdout.line!

    when z is
        @Option (Some str) ->
            Stdout.line! str

        _ ->
            Stdout.line! "No data in the monad"

Richard Feldman (Aug 28 2024 at 05:42):

this sounds familiar - I remember @Ayaz Hafiz mentioning some time ago that there was a missing type constraint somewhere in abilities

Richard Feldman (Aug 28 2024 at 05:43):

actually I think it was in the context of my having tried something similar with streams/iterators :laughing:

Richard Feldman (Aug 28 2024 at 05:43):

and ending up with something that seemed to work but shouldn't

Brendan Hansknecht (Aug 28 2024 at 05:46):

Also, I feel like I may be pointing out two different issue but I am not fully sure. There is a chance that the SequenceWalker and List.walk part should work, but something more flexible in my Monad example should fail to typecheck.

Brendan Hansknecht (Aug 28 2024 at 05:49):

I mean, obviously in the monad example as written, it is using a unconstrained type variable as a Monad. That is definitely incorrect. If ToMonad is added in though and used in the example code, I think that all of the types technically work.

Actually no, even with that change the types technically wouldn't work. mb only implements ToMonad but ToMonad would require it to implement Monad and ToMonad.

Yeah, so this monad example written either way definitely should not work. It is adding abilities to unconstrained type variables.

Brendan Hansknecht (Aug 28 2024 at 05:51):

So yeah, monad version definitely should be broken in type checking.

For SequenceWalker vs List.walk. I don't think the types are technically wrong anywhere. They are just overly generalizing and removing a piece of information. So if you were to type check only based on SequenceWalker, it would allow for types that are invalid for List.walk.

Brendan Hansknecht (Aug 28 2024 at 05:51):

Aside, if we stop SequenceWalker from working, it will definitely limit possibilities for the encoding/decoding api.

Brendan Hansknecht (Aug 28 2024 at 05:52):

I think the root of all of these bugs is that typechecking is done using the concrete types from resolving the ability. This gives way more information that what is specified in the interface of the ability.

Last updated: Jul 06 2025 at 12:14 UTC