Type-level Replicate function

21 Nov 2014

      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:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}

import GHC.TypeLits
import Data.Type.Equality
import Data.Type.Bool

-- For work I'm implementing a binary protocol for
-- communicating with some device. I need to be able to send
-- a packet of orders to a device.
--
-- An order is a list of addresses and command to send to
-- these addresses.
--
-- After sending the packets of orders the device should
-- send back a packet of replies. The packet of replies
-- should have a reply for each command send to each
-- address.
--
-- I would like to make the latter requirement apparent in
-- the types so that when I send a packet of orders the type
-- will tell me what packet of replies to expect.
--
-- So I introduce the OrderPacket type which is
-- parameterised with a type-level lists of commands:
data OrderPacket (cmds :: [*]) where

    -- The empty packet:
    NoOrders :: OrderPacket '[]

    -- Extending an existing packet with an order.
    --
    -- The (n :: Nat) in Order denotes the number of
    -- addresses to send the command to. Note that because I
    -- expect n command replies back I need to create a
    -- type-level list of n commands and prepend that to the
    -- existing commands:
    (:>) :: !(Order n command)
         -> !(OrderPacket commands)
         -> OrderPacket (Replicate n command :++: commands)

-- As explained, an Order is a vector of addresses of length
-- n paired with a command:
data Order (n :: Nat) command where
    Order :: (Command command)
          => !(Addresses n)
          -> !command
          -> Order n command

-- In my real implementation this class describes how to
-- encode / decode commands:
class Command command

-- This is the typical Vector of length n type specialised
-- to Address:
data Addresses (n :: Nat) where
    Nil   :: Addresses 0
    (:*:) :: !Address -> !(Addresses n) -> Addresses (n+1)

infixr 5 :*:

type Address = Int

-- Append two type-level lists.
type family (rs1 :: [*]) :++: (rs2 :: [*]) :: [*]

type instance '[]        :++: rs2 = rs2
type instance (r ': rs1) :++: rs2 = r ': (rs1 :++: rs2)

-- 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)

-- However when I write some code like the following:
isNull :: OrderPacket cmds -> Bool
isNull NoOrders                = True
isNull (orderMsg :> orderMsgs) = False

-- I get the following error:

src/TypeLevelReplicate.hs:49:9:
    Type function application stack overflow; size = 201
    Use -ftype-function-depth=N to increase stack size to N
      GHC.TypeLits.EqNat
        (((n-1)-1)-1)...) 0
      ~ (((n-1)-1)-1)...) == 0)
    In the pattern: orderMsg :> orderMsgs
    In an equation for ‘isNull’:
      isNull (orderMsg :> orderMsgs) = True
Failed, modules loaded: none.

-- Note that when I adapt my code to use my own type-level
-- inductive implementation of natural numbers like:

data N = Z | S N

type family Replicate (n :: N) r :: [*]

type instance Replicate Z     r = '[]
type instance Replicate (S n) r = r ': Replicate n r

-- I don't get the type function application stack overflow.

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

Thanks,

Bas

Type-level Replicate function

Bas van Dijk