Lazy Take?

[treeowl]

I have no idea if it belongs in this package, but one rather handy utility is a lazy take type family:

type LazyTake :: forall k. Nat -> [k] -> [k]
type family LazyTake n xs where
  LazyTake Z _ = '[]
  LazyTake (S n) xs = Head xs : LazyTake n (Tail xs)

This can be used to drive type inference. For example:

-- infer that xs has exactly n elements
xs ~ LazyTake n xs

-- infer that xs has at least n elements
xs ~ LazyTake n xs ++ Drop n xs

-- infer that xs has at least n+1 elements, and that the
-- element at index n is x
xs ~ LazyTake n xs ++ x : Drop (S n) xs