<p dir="ltr">I've replaced the definition of Replicate with a closed type family, and now isNull typechecks on 7.8.2:</p>
<p dir="ltr">type family Replicate (n :: Nat) t : [*] where<br>
  Replicate 0 t = '[]<br>
  Replicate n t = t ': Replicate (n-1) t</p>
<div class="gmail_quote">On Nov 21, 2014 3:52 PM, "Bas van Dijk" <<a href="mailto:v.dijk.bas@gmail.com">v.dijk.bas@gmail.com</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
tl;dr<br>
How do I implement a type-level Replicate function that takes a (n ::<br>
Nat) and a type e and produces a type-level list of n e elements.<br>
<br>
The rest of my email gives some background on why I need this, how<br>
it's supposed to be used and my current erroneous implementation. I'm<br>
presenting it as a Haskell program:<br>
<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE TypeFamilies #-}<br>
{-# LANGUAGE UndecidableInstances #-}<br>
{-# LANGUAGE GADTs #-}<br>
<br>
import GHC.TypeLits<br>
import Data.Type.Equality<br>
import Data.Type.Bool<br>
<br>
-- For work I'm implementing a binary protocol for<br>
-- communicating with some device. I need to be able to send<br>
-- a packet of orders to a device.<br>
--<br>
-- An order is a list of addresses and command to send to<br>
-- these addresses.<br>
--<br>
-- After sending the packets of orders the device should<br>
-- send back a packet of replies. The packet of replies<br>
-- should have a reply for each command send to each<br>
-- address.<br>
--<br>
-- I would like to make the latter requirement apparent in<br>
-- the types so that when I send a packet of orders the type<br>
-- will tell me what packet of replies to expect.<br>
--<br>
-- So I introduce the OrderPacket type which is<br>
-- parameterised with a type-level lists of commands:<br>
data OrderPacket (cmds :: [*]) where<br>
<br>
    -- The empty packet:<br>
    NoOrders :: OrderPacket '[]<br>
<br>
    -- Extending an existing packet with an order.<br>
    --<br>
    -- The (n :: Nat) in Order denotes the number of<br>
    -- addresses to send the command to. Note that because I<br>
    -- expect n command replies back I need to create a<br>
    -- type-level list of n commands and prepend that to the<br>
    -- existing commands:<br>
    (:>) :: !(Order n command)<br>
         -> !(OrderPacket commands)<br>
         -> OrderPacket (Replicate n command :++: commands)<br>
<br>
-- As explained, an Order is a vector of addresses of length<br>
-- n paired with a command:<br>
data Order (n :: Nat) command where<br>
    Order :: (Command command)<br>
          => !(Addresses n)<br>
          -> !command<br>
          -> Order n command<br>
<br>
-- In my real implementation this class describes how to<br>
-- encode / decode commands:<br>
class Command command<br>
<br>
-- This is the typical Vector of length n type specialised<br>
-- to Address:<br>
data Addresses (n :: Nat) where<br>
    Nil   :: Addresses 0<br>
    (:*:) :: !Address -> !(Addresses n) -> Addresses (n+1)<br>
<br>
infixr 5 :*:<br>
<br>
type Address = Int<br>
<br>
-- Append two type-level lists.<br>
type family (rs1 :: [*]) :++: (rs2 :: [*]) :: [*]<br>
<br>
type instance '[]        :++: rs2 = rs2<br>
type instance (r ': rs1) :++: rs2 = r ': (rs1 :++: rs2)<br>
<br>
<br>
-- I'm currently using the following Replicate type-level<br>
-- function:<br>
type family Replicate (n :: Nat) r :: [*]<br>
<br>
type instance Replicate (n :: Nat) r =<br>
    If (n == 0) '[] (r ': Replicate (n-1) r)<br>
<br>
-- However when I write some code like the following:<br>
isNull :: OrderPacket cmds -> Bool<br>
isNull NoOrders                = True<br>
isNull (orderMsg :> orderMsgs) = False<br>
<br>
-- I get the following error:<br>
<br>
src/TypeLevelReplicate.hs:49:9:<br>
    Type function application stack overflow; size = 201<br>
    Use -ftype-function-depth=N to increase stack size to N<br>
      GHC.TypeLits.EqNat<br>
        (((n-1)-1)-1)...) 0<br>
      ~ (((n-1)-1)-1)...) == 0)<br>
    In the pattern: orderMsg :> orderMsgs<br>
    In an equation for ‘isNull’:<br>
      isNull (orderMsg :> orderMsgs) = True<br>
Failed, modules loaded: none.<br>
<br>
-- Note that when I adapt my code to use my own type-level<br>
-- inductive implementation of natural numbers like:<br>
<br>
data N = Z | S N<br>
<br>
type family Replicate (n :: N) r :: [*]<br>
<br>
type instance Replicate Z     r = '[]<br>
type instance Replicate (S n) r = r ': Replicate n r<br>
<br>
-- I don't get the type function application stack overflow.<br>
<br>
Any hints on how to make this work with Nats from GHC.TypeLits?<br>
<br>
Thanks,<br>
<br>
Bas<br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div>