Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | haskelldb-users@lists.sourceforge.net |
Safe Haskell | None |
Database.HaskellDB.BoundedList
Description
The main idea of bounded lists is to create lists with predetermined maximum size.
BoundedList is a simple, fast and type safe approach to implementing this idea. The implementation is based on inductive instances, making it very easy to expand with new bounds. A new bound only requires one instance of size and two instances of Less.
BoundedList works as follows. Every bound is build up by declaring a data-type representing the new bound. The instance of size only returns the size as an Int. The first instance of Less is for telling the typechecker that this bound is greater than the largest smaller bound. The second instance of Less is used by the typechecker to construct a chain of instances if there is no hardcoded instance available. This way the type checker can determine if a bound is smaller/greater then any other bound.
This inductive approach gives the complexity O(n) on the number of instances and very short type checking times compared to an O(n^2) implementation.
BoundedList also comes with a few utility function for manipulation an contructing bounded lists.
To be noted: Since each bound is a unique type: Explicit shrink and/or grow is needed before using (==). BoundedList does not have an instance of Ordering. (This might change)
- shrink :: (Size n, Size m) => BoundedList a n -> Maybe (BoundedList a m)
- grow :: LessEq n m => BoundedList a n -> BoundedList a m
- trunc :: Size n => [a] -> BoundedList a n
- listBound :: Size n => BoundedList a n -> Int
- toBounded :: Size n => [a] -> Maybe (BoundedList a n)
- fromBounded :: Size n => BoundedList a n -> [a]
- class Size n
- data BoundedList a n
- data N0
- data N1
- data N2
- data N3
- data N4
- data N5
- data N6
- data N7
- data N8
- data N9
- data N10
- data N11
- data N12
- data N13
- data N14
- data N15
- data N16
- data N17
- data N18
- data N19
- data N20
- data N21
- data N22
- data N23
- data N24
- data N25
- data N26
- data N27
- data N28
- data N29
- data N30
- data N31
- data N32
- data N33
- data N34
- data N35
- data N36
- data N37
- data N38
- data N39
- data N40
- data N41
- data N42
- data N43
- data N44
- data N45
- data N46
- data N47
- data N48
- data N49
- data N50
- data N51
- data N52
- data N53
- data N54
- data N55
- data N56
- data N57
- data N58
- data N59
- data N60
- data N61
- data N62
- data N63
- data N64
- data N65
- data N66
- data N67
- data N68
- data N69
- data N70
- data N71
- data N72
- data N73
- data N74
- data N75
- data N76
- data N77
- data N78
- data N79
- data N80
- data N81
- data N82
- data N83
- data N84
- data N85
- data N86
- data N87
- data N88
- data N89
- data N90
- data N91
- data N92
- data N93
- data N94
- data N95
- data N96
- data N97
- data N98
- data N99
- data N100
- data N101
- data N102
- data N103
- data N104
- data N105
- data N106
- data N107
- data N108
- data N109
- data N110
- data N111
- data N112
- data N113
- data N114
- data N115
- data N116
- data N117
- data N118
- data N119
- data N120
- data N121
- data N122
- data N123
- data N124
- data N125
- data N126
- data N127
- data N128
- data N129
- data N130
- data N131
- data N132
- data N133
- data N134
- data N135
- data N136
- data N137
- data N138
- data N139
- data N140
- data N141
- data N142
- data N143
- data N144
- data N145
- data N146
- data N147
- data N148
- data N149
- data N150
- data N151
- data N152
- data N153
- data N154
- data N155
- data N156
- data N157
- data N158
- data N159
- data N160
- data N161
- data N162
- data N163
- data N164
- data N165
- data N166
- data N167
- data N168
- data N169
- data N170
- data N171
- data N172
- data N173
- data N174
- data N175
- data N176
- data N177
- data N178
- data N179
- data N180
- data N181
- data N182
- data N183
- data N184
- data N185
- data N186
- data N187
- data N188
- data N189
- data N190
- data N191
- data N192
- data N193
- data N194
- data N195
- data N196
- data N197
- data N198
- data N199
- data N200
- data N201
- data N202
- data N203
- data N204
- data N205
- data N206
- data N207
- data N208
- data N209
- data N210
- data N211
- data N212
- data N213
- data N214
- data N215
- data N216
- data N217
- data N218
- data N219
- data N220
- data N221
- data N222
- data N223
- data N224
- data N225
- data N226
- data N227
- data N228
- data N229
- data N230
- data N231
- data N232
- data N233
- data N234
- data N235
- data N236
- data N237
- data N238
- data N239
- data N240
- data N241
- data N242
- data N243
- data N244
- data N245
- data N246
- data N247
- data N248
- data N249
- data N250
- data N251
- data N252
- data N253
- data N254
- data N255
- data N65535
Documentation
shrink :: (Size n, Size m) => BoundedList a n -> Maybe (BoundedList a m)
Shrinks the BoundedList
supplied if
it can do so without truncating the list. Returns Nothing
if the list inside was to long.
grow :: LessEq n m => BoundedList a n -> BoundedList a m
Takes a BoundedList
add grows it size.
trunc :: Size n => [a] -> BoundedList a n
Takes a list and transforms it to a BoundedList
.
If the list doesn'n fit, the list is truncated
to make it fit into the bounded list.
listBound :: Size n => BoundedList a n -> Int
Returns the length of a BoundedList
.
toBounded :: Size n => [a] -> Maybe (BoundedList a n)
Takes a list and transforms it to a BoundedList
.
If the list doesn't fit, Nothing is returned.
fromBounded :: Size n => BoundedList a n -> [a]
Takes a BoundedList
and return the list inside.
class Size n
Instances
data BoundedList a n
Instances
Typeable (BoundedString n) | |
Size n => ShowConstant (BoundedString n) | |
Size n => ExprType (BoundedString n) | |
Size n => GetValue (Maybe (BoundedString n)) | |
Size n => GetValue (BoundedString n) | |
Size n => BStrToStr (Expr (Maybe (BoundedString n))) (Expr (Maybe String)) | |
Size n => BStrToStr (Expr (BoundedString n)) (Expr String) | |
(Size n, Eq a) => Eq (BoundedList a n) | |
(Show a, Size n) => Show (BoundedList a n) |
data N100
data N101
data N102
data N103
data N104
data N105
data N106
data N107
data N108
data N109
data N110
data N111
data N112
data N113
data N114
data N115
data N116
data N117
data N118
data N119
data N120
data N121
data N122
data N123
data N124
data N125
data N126
data N127
data N128
data N129
data N130
data N131
data N132
data N133
data N134
data N135
data N136
data N137
data N138
data N139
data N140
data N141
data N142
data N143
data N144
data N145
data N146
data N147
data N148
data N149
data N150
data N151
data N152
data N153
data N154
data N155
data N156
data N157
data N158
data N159
data N160
data N161
data N162
data N163
data N164
data N165
data N166
data N167
data N168
data N169
data N170
data N171
data N172
data N173
data N174
data N175
data N176
data N177
data N178
data N179
data N180
data N181
data N182
data N183
data N184
data N185
data N186
data N187
data N188
data N189
data N190
data N191
data N192
data N193
data N194
data N195
data N196
data N197
data N198
data N199
data N200
data N201
data N202
data N203
data N204
data N205
data N206
data N207
data N208
data N209
data N210
data N211
data N212
data N213
data N214
data N215
data N216
data N217
data N218
data N219
data N220
data N221
data N222
data N223
data N224
data N225
data N226
data N227
data N228
data N229
data N230
data N231
data N232
data N233
data N234
data N235
data N236
data N237
data N238
data N239
data N240
data N241
data N242
data N243
data N244
data N245
data N246
data N247
data N248
data N249
data N250
data N251
data N252
data N253
data N254
data N255