I've replaced the definition of Replicate with a closed type family, and
now isNull typechecks on 7.8.2:
type family Replicate (n :: Nat) t : [*] where
Replicate 0 t = '[]
Replicate n t = t ': Replicate (n-1) t
On Nov 21, 2014 3:52 PM, "Bas van Dijk" wrote:
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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
