being generic over List / Array / Stream?

Stream: Is there code for X?

[JJ]

I'd like to write some code generic over all of Lists / Arrays / Streams. The only operation I need on these types is destructuring: match foo with | [] => sorry | head :: tail => sorry, essentially.

Is there any existing typeclass infrastructure around this?

[Yan Yablonovskiy 🇺🇦]

Are you familiar with Monads? You might want to match on pure and bind.

[JJ]

I am not very familiar with monads, no. This is for a project whose goal is to familiarize me with monads and monad transformers actually!

[JJ]

(I've made operational use of monads for years c.f. Option and Result but haven't ever grown the Haskell sense for them)

[JJ]

I have heard that List is the free monad. So I guess Array and Stream are also monads, given their similarity? I'm not quite sure how that ties into an interface around nil and cons, though, hrm. I'll think about it.

[Yan Yablonovskiy 🇺🇦]

List has an instance of LawfulMonad, the situation with Array and Stream are more complicated. For proofs rather than computation, Array has toList. Stream can be even more complicated in general, but if you have non-empty sequences you have docs#Stream'.Seq1 and docs#Stream'.Seq1.lawfulMonad

[Yan Yablonovskiy 🇺🇦]

JJ said:

I have heard that List is the free monad. So I guess Array and Stream are also monads, given their similarity? I'm not quite sure how that ties into an interface around nil and cons, though, hrm. I'll think about it.

You would create an interface for LawfulMonad instead, which then can be applied on a List and more generally since it has such an instance (avoiding reference directly to List specific nil and cons).

[JJ]

I'm not sure I see what Monad/LawfulMonad (I'm not concerned about proof here, so there shouldn't be a difference?) give me in exchange for nil and cons.

Could you explain why Stream is not a monad (when empty) but List is?

[JJ]

Oh, this is interesting. #general > question: why List is nolonger Monad?

[Alfredo Moreira-Rosa]

You have ForIn that should work to iterate in a generic way (so only destructuring current folded item), for example :

def printAll {t : Type → Type} {α} [ToString α] [ForIn IO (t α) α] (xs : t α) : IO Unit := do
  for x in xs do
    IO.println (toString x)


-- List
#eval printAll [1,2,3] -- 1\n2\n3
-- Array
#eval printAll #[1,2,3] -- 1\n2\n3]
-- Stream
#eval printAll (Std.ToStream.toStream [1,2,3]) -- 1\n2\n3

[Jovan Gerbscheid]

I think the new iterator library is meant to help with your problem. A list/Array can be turned into an iterator, and then the iterator can be passed to your "generic" function.