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
I have no idea if it belongs in this package, but one rather handy utility is a lazy take type family:
This can be used to drive type inference. For example: