Lazy Take?

[treeowl]

The following type family is often useful:

type LazyTake :: Nat -> [k] -> [k]
type family LazyTake n xs where
  LazyTake 0 _ = '[]
  LazyTake n xs = Head xs ': LazyTake (n - 1) (Tail xs)

This is a promoted version of the (partial) function

lazyTake :: Natural -> [a] -> [a]
lazyTake 0 _ = []
lazyTake n xs = head xs : lazyTake (n - 1) (tail xs)

It's useful in constructions like

type LengthAtLeast n xs = xs ~ LazyTake n xs ++ Drop n xs

I imagine this package is not the one such a thing belongs in; any guess where I might find it, or where it might fit?

[RyanGlScott]

I'm not aware of any package that provides this.

Out of curiosity, does defining this lazily actually make a difference in practice on the type level? I was under the impression that the order of evaluation in type family equations wasn't specified.

[treeowl]

Oh yes, definitely. The reduction semantics are not fully specified:

type family Loop :: [Bool] where
  Loop = Loop

> :kind LazyTake 0 Loop
-- unspecified result

However, LazyTake will definitely make progress if its list argument is not looping but merely stuck, polymorphic, or ambiguous.

type family Stuck :: [Bool] where
> :kind! LazyTake 0 Stuck
'[]
> :kind! LazyTake 2 Stuck
'[Head Stuck, Head (Tail Stuck)]

If I'm not very much mistaken, TypeError applications are treated as stuck unless and until GHC concludes that type checking has failed, so

> :kind! LazyTake 0 (TypeError ...)
'[]
> :kind! Length (LazyTake 2 (TypeError ...))
2
> :kind! LazyTake 2 (TypeError ...)
<Uh oh some errors>

In practice, the irretrievably stuck and type error cases are rather dull; reduction will make progress but usually fail somewhere else. But the ambiguous and polymorphic cases can allow useful type information to flow.

[RyanGlScott]

I see, that is surprisingly nuanced.

To be honest, I'm not even sure if there is a Haskell library that provides a term-level lazyTake, let alone a type-level one, so I can't offer any suggestions on where to look.

[treeowl]

Not everything useful at the type level is equally useful at the term level. I rarely want Take at the type level; I rarely, if ever, want lazyTake at the term level.

Disclosure: in what I'm actually working on, we're using inductive naturals instead of garbage ones (except at the edges of the API), so I wouldn't likely use a GHC Nat version anyway.