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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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 On Nov 21, 2014 3:52 PM, "Bas van Dijk" <[hidden email]> wrote:
Hi, _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Bas van Dijk-2
Bas van Dijk <[hidden email]> 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 _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Dr. ERDI Gergo
On 21 November 2014 09:21, Dr. ÉRDI Gergő <[hidden email]> wrote:
> 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 Thanks that works beautifully! _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Antonio Nikishaev-2
On 21 November 2014 09:35, Antonio Nikishaev <[hidden email]> wrote:
> type instance Replicate (n :: Nat) r = > If (n == 0) '[] (r ': Replicate (If (n==0) 0 (n-1)) r) Interesting! _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Free forum by Nabble | Edit this page |