Type-level Replicate function

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Type-level Replicate function

Bas van Dijk-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Type-level Replicate function

Dr. ERDI Gergo

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" <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Type-level Replicate function

Antonio Nikishaev-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Type-level Replicate function

Bas van Dijk-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Type-level Replicate function

Bas van Dijk-2
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