parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2017-2019
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.List

Contents

- Constants

Description

This module defines a list over two parameters. The first is a fixed type-level function `k -> *` for some kind `k`, and the second is a list of types with kind `k` that provide the indices for the values in the list.

This type is closely related to the `Assignment` type in Data.Parameterized.Context.

# Motivating example - the `List` type

For this example, we need the following extensions:

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE TypeOperators #-}

We also require the following imports:

    import Data.Parameterized
    import Data.Parameterized.List
    import GHC.TypeLits

Suppose we have a bitvector type:

    data BitVector (w :: Nat) :: * where
      BV :: NatRepr w -> Integer -> BitVector w

This type contains a `NatRepr`, a value-level representative of the vector width, and an `Integer`, containing the actual value of the bitvector. We can create values of this type as follows:

    BV (knownNat @8) 0xAB

We can also create a smart constructor to handle the `NatRepr` automatically, when the width is known from the type context:

    bitVector :: KnownNat w => Integer -> BitVector w
    bitVector x = BV knownNat x

Note that this does not check that the value can be represented in the given number of bits; that is not important for this example.

If we wish to construct a list of `BitVector`s of a particular length, we can do:

    [bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8

However, what if we wish to construct a list of `BitVector`s of different lengths? We could try:

    [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]

However, this gives us an error:

    <interactive>:3:33: error:
        • Couldn't match type ‘16’ with ‘8’
          Expected type: BitVector 8
            Actual type: BitVector 16
        • In the expression: bitVector 0x1234 :: BitVector 16
          In the expression:
            [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
          In an equation for ‘it’:
              it
                = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]

A vanilla Haskell list cannot contain two elements of different types, and even though the two elements here are both `BitVector`s, they do not have the same type! One solution is to use the `Some` type:

    [Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]

The type of the above expression is `[Some BitVector]`, which may be perfectly acceptable. However, there is nothing in this type that tells us what the widths of the bitvectors are, or what the length of the overall list is. If we want to actually track that information on the type level, we can use the `List` type from this module.

    (bitVector 0xAB :: BitVector 8) :< (bitVector 0x1234 :: BitVector 16) :< Nil

The type of the above expression is `List BitVector '[8, 16]` -- That is, a two-element list of `BitVector`s, where the first element has width 8 and the second has width 16.

## Summary

In general, if we have a type constructor `Foo` of kind `k -> *` (in our example, `Foo` is just `BitVector`, and we want to create a list of `Foo`s where the parameter `k` varies, and we wish to keep track of what each value of `k` is inside the list at compile time, we can use the `List` type for this purpose.

Synopsis

- data List (a :: k -> Type) (b :: [k]) where
  - Nil :: forall {k} (a :: k -> Type). List a ('[] :: [k])
  - (:<) :: forall {k} (a :: k -> Type) (tp :: k) (tps :: [k]). a tp -> List a tps -> List a (tp ': tps)
- fromSomeList :: forall {k} (f :: k -> Type). [Some f] -> Some (List f)
- fromListWith :: forall {k} a (f :: k -> Type). (a -> Some f) -> [a] -> Some (List f)
- fromListWithM :: forall {k} a (f :: k -> Type) m. Monad m => (a -> m (Some f)) -> [a] -> m (Some (List f))
- data Index (a :: [k]) (b :: k) where
  - IndexHere :: forall {k} (b :: k) (r :: [k]). Index (b ': r) b
  - IndexThere :: forall {k} (r :: [k]) (b :: k) (x :: k). !(Index r b) -> Index (x ': r) b
- indexValue :: forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer
- (!!) :: forall {k} f (l :: [k]) (x :: k). List f l -> Index l x -> f x
- update :: forall {k} f (l :: [k]) (s :: k). List f l -> Index l s -> (f s -> f s) -> List f l
- indexed :: forall {k} (l :: [k]) (x :: k) (f :: k -> Type). Index l x -> Lens' (List f l) (f x)
- imap :: forall {k} f g (l :: [k]). (forall (x :: k). Index l x -> f x -> g x) -> List f l -> List g l
- ifoldlM :: forall {k} (sh :: [k]) a b m. Monad m => (forall (tp :: k). b -> Index sh tp -> a tp -> m b) -> b -> List a sh -> m b
- ifoldr :: forall {k} (sh :: [k]) a b. (forall (tp :: k). Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b
- izipWith :: forall {k} a b c (sh :: [k]). (forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp) -> List a sh -> List b sh -> List c sh
- itraverse :: forall {k} a b (sh :: [k]) t. Applicative t => (forall (tp :: k). Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh)
- index0 :: forall {k} (x :: k) (r :: [k]). Index (x ': r) x
- index1 :: forall {k} (x0 :: k) (x1 :: k) (r :: [k]). Index (x0 ': (x1 ': r)) x1
- index2 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': r))) x2
- index3 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (x3 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': (x3 ': r)))) x3

# Documentation

data List (a :: k -> Type) (b :: [k]) where Source #

Parameterized list of elements.

Constructors

Nil :: forall {k} (a :: k -> Type). List a ('[] :: [k]) |
(:<) :: forall {k} (a :: k -> Type) (tp :: k) (tps :: [k]). a tp -> List a tps -> List a (tp ': tps) infixr 5 |

#### Instances

Instances details

FoldableFC (List :: (k -> Type) -> [k] -> Type) Source # |

Instance details

Defined in Data.Parameterized.List

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: [k]). List f x -> m Source #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: [k]). b -> List f x -> b Source #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: [k]). b -> List f x -> b Source #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: [k]). b -> List f x -> b Source #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: [k]). b -> List f x -> b Source #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: [k]). List f x -> [a] Source #

FunctorFC (List :: (k -> Type) -> [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: [k]). List f x -> List g x Source #
TraversableFC (List :: (k -> Type) -> [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: [k]). List f x -> m (List g x) Source #
FoldableFCWithIndex (List :: (k -> Type) -> [k] -> Type) Source # |

Instance details

Defined in Data.Parameterized.List

Methods

ifoldMapFC :: forall f m (z :: [k]). Monoid m => (forall (x :: k). IndexF (List f z) x -> f x -> m) -> List f z -> m Source #

ifoldrFC :: forall (z :: [k]) f b. (forall (x :: k). IndexF (List f z) x -> f x -> b -> b) -> b -> List f z -> b Source #

ifoldlFC :: forall f b (z :: [k]). (forall (x :: k). IndexF (List f z) x -> b -> f x -> b) -> b -> List f z -> b Source #

ifoldrFC' :: forall f b (z :: [k]). (forall (x :: k). IndexF (List f z) x -> f x -> b -> b) -> b -> List f z -> b Source #

ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: [k]). b -> List f x -> b Source #

itoListFC :: forall f a (z :: [k]). (forall (x :: k). IndexF (List f z) x -> f x -> a) -> List f z -> [a] Source #

FunctorFCWithIndex (List :: (k -> Type) -> [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods imapFC :: forall f g (z :: [k]). (forall (x :: k). IndexF (List f z) x -> f x -> g x) -> List f z -> List g z Source #
TraversableFCWithIndex (List :: (k -> Type) -> [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods itraverseFC :: forall m (z :: [k]) f g. Applicative m => (forall (x :: k). IndexF (List f z) x -> f x -> m (g x)) -> List f z -> m (List g z) Source #
TestEquality f => TestEquality (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) Source #
EqF f => EqF (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods eqF :: forall (a :: [k]). List f a -> List f a -> Bool Source #
OrdF f => OrdF (List f :: [k] -> Type) Source # |

Instance details

Defined in Data.Parameterized.List

Methods

compareF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> OrderingF x y Source #

leqF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> Bool Source #

ltF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> Bool Source #

geqF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> Bool Source #

gtF :: forall (x :: [k]) (y :: [k]). List f x -> List f y -> Bool Source #

ShowF f => ShowF (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods withShow :: forall p q (tp :: [k]) a. p (List f) -> q tp -> (Show (List f tp) => a) -> a Source # showF :: forall (tp :: [k]). List f tp -> String Source # showsPrecF :: forall (tp :: [k]). Int -> List f tp -> String -> String Source #
IsRepr f => IsRepr (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: [k]) r. List f a -> (KnownRepr (List f) a => r) -> r Source #
KnownRepr (List f :: [k] -> Type) ('[] :: [k]) Source # |
Instance details Defined in Data.Parameterized.List Methods knownRepr :: List f ('[] :: [k]) Source #
(KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f :: [a] -> Type) (s ': sh :: [a]) Source # |
Instance details Defined in Data.Parameterized.List Methods knownRepr :: List f (s ': sh) Source #
ShowF f => Show (List f sh) Source # |
Instance details Defined in Data.Parameterized.List Methods showsPrec :: Int -> List f sh -> ShowS Source # show :: List f sh -> String Source # showList :: [List f sh] -> ShowS Source #
type IndexF (List f sh) Source # |
Instance details Defined in Data.Parameterized.List type IndexF (List f sh) = Index sh
type IxValueF (List f sh) Source # |
Instance details Defined in Data.Parameterized.List type IxValueF (List f sh) = f

fromSomeList :: forall {k} (f :: k -> Type). [Some f] -> Some (List f) Source #

Map from list of Some to Some list

fromListWith :: forall {k} a (f :: k -> Type). (a -> Some f) -> [a] -> Some (List f) Source #

Apply function to list to yield a parameterized list.

fromListWithM :: forall {k} a (f :: k -> Type) m. Monad m => (a -> m (Some f)) -> [a] -> m (Some (List f)) Source #

Apply monadic action to list to yield a parameterized list.

data Index (a :: [k]) (b :: k) where Source #

Represents an index into a type-level list. Used in place of integers to 1. ensure that the given index *does* exist in the list 2. guarantee that it has the given kind

Constructors

IndexHere :: forall {k} (b :: k) (r :: [k]). Index (b ': r) b |
IndexThere :: forall {k} (r :: [k]) (b :: k) (x :: k). !(Index r b) -> Index (x ': r) b |

#### Instances

Instances details

TestEquality (Index l :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) Source #
OrdF (Index l :: k -> Type) Source # |

Instance details

Defined in Data.Parameterized.List

Methods

compareF :: forall (x :: k) (y :: k). Index l x -> Index l y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). Index l x -> Index l y -> Bool Source #

ltF :: forall (x :: k) (y :: k). Index l x -> Index l y -> Bool Source #

geqF :: forall (x :: k) (y :: k). Index l x -> Index l y -> Bool Source #

gtF :: forall (x :: k) (y :: k). Index l x -> Index l y -> Bool Source #

ShowF (Index l :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods withShow :: forall p q (tp :: k) a. p (Index l) -> q tp -> (Show (Index l tp) => a) -> a Source # showF :: forall (tp :: k). Index l tp -> String Source # showsPrecF :: forall (tp :: k). Int -> Index l tp -> String -> String Source #
Show (Index l x) Source # |
Instance details Defined in Data.Parameterized.List Methods showsPrec :: Int -> Index l x -> ShowS Source # show :: Index l x -> String Source # showList :: [Index l x] -> ShowS Source #
Eq (Index l x) Source # |
Instance details Defined in Data.Parameterized.List Methods (==) :: Index l x -> Index l x -> Bool Source # (/=) :: Index l x -> Index l x -> Bool Source #
Ord (Index sh x) Source # |

Instance details

Defined in Data.Parameterized.List

Methods

compare :: Index sh x -> Index sh x -> Ordering Source #

(<) :: Index sh x -> Index sh x -> Bool Source #

(<=) :: Index sh x -> Index sh x -> Bool Source #

(>) :: Index sh x -> Index sh x -> Bool Source #

(>=) :: Index sh x -> Index sh x -> Bool Source #

max :: Index sh x -> Index sh x -> Index sh x Source #

min :: Index sh x -> Index sh x -> Index sh x Source #

Hashable (Index l x) Source # |
Instance details Defined in Data.Parameterized.List Methods hashWithSalt :: Int -> Index l x -> Int Source # hash :: Index l x -> Int Source #

indexValue :: forall {k} (l :: [k]) (tp :: k). Index l tp -> Integer Source #

Return the index as an integer.

(!!) :: forall {k} f (l :: [k]) (x :: k). List f l -> Index l x -> f x Source #

Return the value in a list at a given index

update :: forall {k} f (l :: [k]) (s :: k). List f l -> Index l s -> (f s -> f s) -> List f l Source #

Update the `List` at an index

indexed :: forall {k} (l :: [k]) (x :: k) (f :: k -> Type). Index l x -> Lens' (List f l) (f x) Source #

Provides a lens for manipulating the element at the given index.

imap :: forall {k} f g (l :: [k]). (forall (x :: k). Index l x -> f x -> g x) -> List f l -> List g l Source #

Map over the elements in the list, and provide the index into each element along with the element itself.

This is a specialization of `imapFC`.

ifoldlM :: forall {k} (sh :: [k]) a b m. Monad m => (forall (tp :: k). b -> Index sh tp -> a tp -> m b) -> b -> List a sh -> m b Source #

Left fold with an additional index.

ifoldr :: forall {k} (sh :: [k]) a b. (forall (tp :: k). Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b Source #

Right-fold with an additional index.

This is a specialization of `ifoldrFC`.

izipWith :: forall {k} a b c (sh :: [k]). (forall (tp :: k). Index sh tp -> a tp -> b tp -> c tp) -> List a sh -> List b sh -> List c sh Source #

Zip up two lists with a zipper function, which can use the index.

itraverse :: forall {k} a b (sh :: [k]) t. Applicative t => (forall (tp :: k). Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh) Source #

Traverse with an additional index.

This is a specialization of `itraverseFC`.

# Constants

index0 :: forall {k} (x :: k) (r :: [k]). Index (x ': r) x Source #

Index 0

index1 :: forall {k} (x0 :: k) (x1 :: k) (r :: [k]). Index (x0 ': (x1 ': r)) x1 Source #

Index 1

index2 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': r))) x2 Source #

Index 2

index3 :: forall {k} (x0 :: k) (x1 :: k) (x2 :: k) (x3 :: k) (r :: [k]). Index (x0 ': (x1 ': (x2 ': (x3 ': r)))) x3 Source #

Index 3