parameterized-utils-2.1.2.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2017-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

Data.Parameterized.List

Contents

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 BitVectors 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 BitVectors 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 BitVectors, 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 BitVectors, 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 Foos 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

Documentation

data List :: (k -> *) -> [k] -> * where Source #

Parameterized list of elements.

Constructors

Nil :: List f '[] 
(:<) :: f tp -> List f tps -> List f (tp ': tps) infixr 5 

Instances

Instances details
TraversableFC (List :: (k -> Type) -> [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). List f x -> m (List g x) Source #

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

Defined in Data.Parameterized.List

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). List f x -> m Source #

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> List f x -> b Source #

foldlFC :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> List f x -> b Source #

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> List f x -> b Source #

foldlFC' :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> List f x -> b Source #

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

FunctorFC (List :: (k -> Type) -> [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). List f x -> List g x Source #

TestEquality f => TestEquality (List f :: [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: k0) (b :: k0). List f a -> List f b -> Maybe (a :~: b) #

ShowF f => ShowF (List f :: [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

withShow :: forall p q (tp :: k0) a. p (List f) -> q tp -> (Show (List f tp) => a) -> a Source #

showF :: forall (tp :: k0). List f tp -> String Source #

showsPrecF :: forall (tp :: k0). Int -> List f tp -> String -> String Source #

OrdF f => OrdF (List f :: [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

compareF :: forall (x :: k0) (y :: k0). List f x -> List f y -> OrderingF x y Source #

leqF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source #

ltF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source #

geqF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source #

gtF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source #

IsRepr f => IsRepr (List f :: [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k0) 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 '[] 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 #

show :: List f sh -> String #

showList :: [List f sh] -> ShowS #

data Index :: [k] -> 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 :: Index (x ': r) x 
IndexThere :: !(Index r y) -> Index (x ': r) y 

Instances

Instances details
TestEquality (Index l :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: k0) (b :: k0). Index l a -> Index l b -> Maybe (a :~: b) #

ShowF (Index l :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

withShow :: forall p q (tp :: k0) a. p (Index l) -> q tp -> (Show (Index l tp) => a) -> a Source #

showF :: forall (tp :: k0). Index l tp -> String Source #

showsPrecF :: forall (tp :: k0). Int -> Index l tp -> String -> String Source #

OrdF (Index l :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

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

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

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

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

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

Eq (Index l x) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

(==) :: Index l x -> Index l x -> Bool #

(/=) :: Index l x -> Index l x -> Bool #

Ord (Index sh x) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

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

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

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

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

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

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

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

Show (Index l x) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

showsPrec :: Int -> Index l x -> ShowS #

show :: Index l x -> String #

showList :: [Index l x] -> ShowS #

Hashable (Index l x) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

hashWithSalt :: Int -> Index l x -> Int #

hash :: Index l x -> Int #

indexValue :: Index l tp -> Integer Source #

Return the index as an integer.

(!!) :: List f l -> Index l x -> f x Source #

Return the value in a list at a given index

update :: List f l -> Index l s -> (f s -> f s) -> List f l Source #

Update the List at an index

indexed :: Index l x -> Lens' (List f l) (f x) Source #

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

imap :: forall f g l. (forall x. 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.

ifoldr :: forall sh a b. (forall tp. Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b Source #

Right-fold with an additional index.

izipWith :: forall a b c sh. (forall tp. 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 a b sh t. Applicative t => (forall tp. Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh) Source #

Traverse with an additional index.

Constants

index0 :: Index (x ': r) x Source #

Index 0

index1 :: Index (x0 ': (x1 ': r)) x1 Source #

Index 1

index2 :: Index (x0 ': (x1 ': (x2 ': r))) x2 Source #

Index 2

index3 :: Index (x0 ': (x1 ': (x2 ': (x3 ': r)))) x3 Source #

Index 3