singletons
singletons copied to clipboard
goldfirere
Lazy Take?
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?
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.
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.
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.
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.