bus.lhs

# Context

I'm writing a small library for modelling digital logic using
FRP-style behaviours. The core type is a Node:

>   type Node = Integer -> Bool

which represents a boolean value varying over integral timesteps.

I also want to model a bus (a fixed-width array) of nodes, using a type-safe
system based on type-level numerals. For example:

>   twoBitWideBus :: Bus Two
>   fourBitWideBus :: Bus Four
>   
>   -- These two types are different, and so the following should cause a type error:
>   f :: Bus Two -> a
>   g = f fourBitWideBus

Since the majority of digital binary systems use buses with widths that are
powers of two, the numerals will be based on a doubling function rather than a
successor function:

>   data One
>   data Twice a

>   type Two = Twice One
>   type Four = Twice Two
>   type Eight = Twice Four
>   -- etc.

Internally, buses would be represented as some form of set of nodes, and should
contain exactly the same number of nodes as specified by its type parameter.
Functions such as the following would ideally be implemented.

>   -- Find the width of a given Bus (i.e. convert from type-level to value-level)
>   widthOf :: Bus n -> Integer

>   -- Convert a list of Nodes into a Bus, throwing an error if the list is the
>   -- wrong length if possible. The width of the Bus should be determined by
>   -- the context the return value is used in.
>   compose :: [Node] -> Bus n

>   -- Opposite of compose.
>   decompose :: Bus n -> [Node]

## The Question

My question is this: how could the Bus type and its associated functions be
implemented? I'm sure that it would involve GADTs, type families and/or
associated types, and there may be multiple possible solutions.

## My (failed) attempts

### Using type families

>   data family Bus n

>   data instance Bus One = SingletonBus Node

>   data instance Bus (Twice n) = PairBus (Bus n) (Bus n)

>   widthOf :: Bus n -> Integer
>   widthOf (SingletonBus node) = 1
>   widthOf (PairBus a b)       = 2 * widthOf a

>   compose :: [Node] -> Bus n
>   compose []     = error "List is not a multiple of two"
>   compose [node] = SingletonBus node
>   compose nodes  = let (a, b) = splitAt (length nodes `div` 2) nodes
>                    in  PairBus (compose a) (compose b)

>   decompose :: Bus n -> [Node]
>   decompose (SingletonBus node) = [node]
>   decompose (PairBus a b) = decompose a ++ decompose b

### Using type classes

Although this seems (to me) to be the easiest and most likely method to work,
it's not a generalised type as I would prefer - this method requires me to put
`(Bus b) =>` into every context that a bus is used in.

>   class Bus b where
>       widthOf :: b -> Integer
>       compose :: [Node] -> b
>       decompose :: b -> [Node]

>   instance Bus SingletonBus where
>       widthOf = const 1
>       compose [node] = SingletonBus node
>       compose _ = error "Expected list of length 1"
>       decompose (SingletonBus node) = [node]

>   instance Bus PairBus where
>       widthOf (PairBus a _) = 2 * widthOf a
>       compose nodes = let (a, b) = splitAt (length nodes `div` 2) nodes
>                       in  PairBus (compose a) (compose b)
>       decompose (PairBus a b) = decompose a ++ decompose b

Error I get when compiling type families code:

logic.lhs:61:14:
    Couldn't match type `One' with `Twice n2'
    Expected type: Bus n
      Actual type: Bus (Twice n2)
    In the pattern: PairBus a b
    In an equation for `widthOf': widthOf (PairBus a b) = 2 * widthOf a

logic.lhs:67:26:
    Couldn't match type `One' with `Twice n1'
    Expected type: Bus n
      Actual type: Bus (Twice n1)
    In the return type of a call of `PairBus'
    In the expression: PairBus (compose a) (compose b)
    In the expression:
      let (a, b) = splitAt (length nodes `div` 2) nodes
      in PairBus (compose a) (compose b)

logic.lhs:71:16:
    Couldn't match type `One' with `Twice n0'
    Expected type: Bus n
      Actual type: Bus (Twice n0)
    In the pattern: PairBus a b
    In an equation for `decompose':
        decompose (PairBus a b) = decompose a ++ decompose b