# Basic lazy sequence abstraction,
# using a thunk to calculate the rest.
Seq a : [
        Seq { first : a, rest : ({} -> Seq a) },
        EofSeq
    ]

# A NonEmptySeq always has an element,
# but getting the rest is just a regular seq.
# Because of structural equality, this _is_
# a Seq.
NonEmptySeq a b : [
        Seq { first : a, rest : ({} -> Seq a) }
    ]b

# An infinite seq never has an `EofSeq`
# Because of structural equality, this is
# both a NonEmptySeq and a Seq.
InfiniteSeq a b : [
        Seq { first : a, rest : ({} -> InfiniteSeq a) }
    ]b

# Isn't really correct without List.drop or equivalent.
seqFromList : List a -> Seq a
seqFromList = \ xs ->
    when List.get xs 0 is
        # \ {} -> seqFromList (List.drop xs 1)
        Ok first -> Seq { first, rest: \ {} -> seqFromList xs }
        _ -> EofSeq

# Creates an infinite lazy Seq filled with xs.
repeateInfinite : a -> InfiniteSeq a *
repeateInfinite = \ x ->
    Seq { first: x, rest: \ {} -> repeateInfinite x }

# Length of any Seq
# Dummy implementation, only for testing the types
seqLen : Seq a -> Nat
seqLen = \ _s -> 0

# Gets the head of a NonEmptySeq or an InfiniteSeq
# Always guaranteed to work, no Result here
firstOfNonEmpty : NonEmptySeq a * -> a
firstOfNonEmpty = \ sq ->
    when sq is
        Seq { first } -> first

## Testcases

test : NonEmptySeq Str *
test = Seq { first: "Ikke-tom", rest: \ {} -> EofSeq }

# Can get the length of both Seq and NonEmptySeq even
# though it is implemented in terms of Seq
len : Nat
len = seqLen test

frst : Str
frst = firstOfNonEmpty test

# Can get the first element of an InfiniteSeq, even
# though it's implemented in terms of NonEmptySeq
fsrrst : Str
fsrrst = firstOfNonEmpty (repeateInfinite "Hei")