Type-level Replicate function

[Antonio Nikishaev]

Bas van Dijk <v.dijk.bas at gmail.com> writes:

> Hi,
>
> tl;dr
> How do I implement a type-level Replicate function that takes a (n ::
> Nat) and a type e and produces a type-level list of n e elements.
>
> The rest of my email gives some background on why I need this, how
> it's supposed to be used and my current erroneous implementation. I'm
> presenting it as a Haskell program:

[...]

> -- I'm currently using the following Replicate type-level
> -- function:
> type family Replicate (n :: Nat) r :: [*]
>
> type instance Replicate (n :: Nat) r =
>     If (n == 0) '[] (r ': Replicate (n-1) r)

type instance Replicate (n :: Nat) r =
    If (n == 0) '[] (r ': Replicate (If (n==0) 0 (n-1)) r)


> Any hints on how to make this work with Nats from GHC.TypeLits?



-- lelf