Popularity
2.6
Declining
Activity
0.0
Stable
2
2
1
Monthly Downloads: 20
Programming language: Haskell
License: BSD 3-clause "New" or "Revised" License
Latest version: v0.5
expressions alternatives and similar packages
Based on the "Data" category.
Alternatively, view expressions alternatives based on common mentions on social networks and blogs.
-
semantic-source
Parsing, analyzing, and comparing source code across many languages -
lens
Lenses, Folds, and Traversals - Join us on web.libera.chat #haskell-lens -
code-builder
Packages for defining APIs, running them, generating client code and documentation. -
text
Haskell library for space- and time-efficient operations over Unicode text. -
cassava
A CSV parsing and encoding library optimized for ease of use and high performance -
unordered-containers
Efficient hashing-based container types -
compendium-client
Mu (μ) is a purely functional framework for building micro services. -
holmes
A reference library for constraint-solving with propagators and CDCL. -
binary
Efficient, pure binary serialisation using ByteStrings in Haskell. -
resource-pool
A high-performance striped resource pooling implementation for Haskell -
primitive
This package provides various primitive memory-related operations. -
discrimination
Fast linear time sorting and discrimination for a large class of data types -
audiovisual
Extensible records, variants, structs, effects, tangles -
IORefCAS
A collection of different packages for CAS based data structures. -
dependent-sum
Dependent sums and supporting typeclasses for comparing and displaying them -
reflection
Reifies arbitrary Haskell terms into types that can be reflected back into terms -
dependent-map
Dependently-typed finite maps (partial dependent products) -
streaming
An optimized general monad transformer for streaming applications, with a simple prelude of functions -
orgmode-parse
Attoparsec parser combinators for parsing org-mode structured text! -
safecopy
An extension to Data.Serialize with built-in version control -
text-icu
This package provides the Haskell Data.Text.ICU library, for performing complex manipulation of Unicode text. -
scientific
Arbitrary-precision floating-point numbers represented using scientific notation -
uuid-types
A Haskell library for creating, printing and parsing UUIDs
Build time-series-based applications quickly and at scale.
InfluxDB is the Time Series Platform where developers build real-time applications for analytics, IoT and cloud-native services. Easy to start, it is available in the cloud or on-premises.
Promo
www.influxdata.com
Do you think we are missing an alternative of expressions or a related project?
README
expressions
λ> :set -XDataKinds -XFlexibleContexts -XKindSignatures -XOverloadedStrings -XRankNTypes -XTypeOperators
λ> import Data.Expression as E
λ> import Data.Maybe
λ> import Data.Singletons
λ> import Data.Text
defining expressions
λ> var "a" .+. var "b" :: ALia 'IntegralSort
(+ (a : int) (b : int))
λ> :{
let a, b, c, d, x, y, z, i :: forall f (s :: Sort). ( VarF :<: f, SingI s ) => IFix f s
a = var "a"
b = var "b"
c = var "c"
d = var "d"
x = var "x"
y = var "y"
z = var "z"
i = var "i"
:}
λ> select a (i :: ALia 'IntegralSort) .+. b :: ALia 'IntegralSort
(+ (select (a : array int int) (i : int)) (b : int))
parsing expressions
λ> :{
let in1, in2, in3 :: Text
in1 = "(select (a : array int (array int bool)) (+ (b : int) 3))"
in2 = "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))"
in3 = "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"
:}
λ> parse in1 :: Maybe (QFALia ('ArraySort 'IntegralSort 'BooleanSort))
Just (select (a : array int (array int bool)) (+ 3 (b : int)))
λ> parse in2 :: Maybe (Lia 'BooleanSort)
Just (forall ((x : int)) (exists ((y : int)) (= (b : bool) (< (x : int) (y : int)))))
λ> parse in3 :: Maybe (Lia 'BooleanSort)
Just (and (forall ((x : int) (y : int)) (< (x : int) (+ (y : int) (z : int)))) (= (z : int) 3))
equating expressions
λ> a == (fromJust $ parse "(a : int)" :: ALia 'IntegralSort)
True
λ> a == (fromJust $ parse "(+ (a : int) 3)" :: ALia 'IntegralSort)
False
λ> a .+. cnst 1 == (fromJust $ parse "(+ (a : int) 1)" :: ALia 'IntegralSort)
True
substituting
λ> (a .*. (a .+. cnst 3) :: ALia 'IntegralSort) `substitute` (cnst 3 `for` (a .+. cnst 3))
(* (a : int) 3)
listing variables
λ> :{
let ai, bi :: Var 'IntegralSort
ai = a
bi = b
qe :: Lia 'BooleanSort
qe = forall [ai] (exists [bi] (a .+. b .=. c .+. d))
:}
λ> vars qe
[(a : int),(b : int),(c : int),(d : int)]
λ> freevars qe
[(c : int),(d : int)]
distinguish quantifier-free from quantified formulae
λ> isQuantified (z .&. (exists [b :: Var 'IntegralSort] (a .+. b .=. c .+. d)) :: Lia 'BooleanSort)
True
λ> isQuantifierFree (z .&. a .+. b .=. c .+. d :: Lia 'BooleanSort)
True
negation normal form
λ> nnf (E.not (z .&. (exists [b :: Var 'IntegralSort] (a .+. b .=. c .+. d)) :: Lia 'BooleanSort))
(or (not (z : bool)) (forall ((b : int)) (not (= (+ (a : int) (b : int)) (+ (c : int) (d : int))))))
prenex form
λ> :{
let cb :: Var 'BooleanSort
cb = c
di :: Var 'IntegralSort
di = d
qe :: Lia 'BooleanSort
qe = forall [ai] (b .&. E.not (exists [cb] (c .->. d)) .&. forall [di] (d .+. a ./=. cnst 3))
:}
λ> prenex qe
(forall
((f2 : int) (f1 : int))
(forall
((f0 : bool))
(and
(b : bool)
(and (f0 : bool) (not (d : bool)))
(not (= (+ (f1 : int) (f2 : int)) 3))
)
)
)
flat form
λ> flatten (select a (i .+. cnst 1) .=. cnst 3 :: ALia 'BooleanSort)
(exists ((k0 : int)) (and (= (k0 : int) (+ 1 (i : int))) (= (select (a : array int int) (k0 : int)) 3)))
λ> type L1 = UniversalF ('ArraySort 'IntegralSort 'IntegralSort) :+: ALiaF
λ> flatten (select (store a i (cnst 3)) (cnst 4) .=. b :: IFix L1 'BooleanSort)
(forall
((k0 : array int int))
(or
(not (= (k0 : array int int) (store (a : array int int) (i : int) 3)))
(= (select (k0 : array int int) 4) (b : int))
)
)
λ> type L2 = ExistentialF ('ArraySort 'IntegralSort 'IntegralSort) :+: L1
λ> flatten (select (store a i (cnst 3)) (cnst 4) .=. b :: IFix L2 'BooleanSort)
(exists
((k0 : array int int))
(and
(= (k0 : array int int) (store (a : array int int) (i : int) 3))
(= (select (k0 : array int int) 4) (b : int))
)
)
replace store terms using axiom
λ> unstore (select (store a i (cnst 3)) (cnst 4) .=. b :: IFix L2 'BooleanSort)
(exists
((k0 : array int int))
(and
(and
(= (select (k0 : array int int) (i : int)) 3)
(forall
((m0 : int))
(or
(= (i : int) (m0 : int))
(= (select (k0 : array int int) (m0 : int)) (select (a : array int int) (m0 : int)))
)
)
)
(= (select (k0 : array int int) 4) (b : int))
)
)
See documentation.