mirror of
https://github.com/coot/free-category.git
synced 2024-11-22 16:22:05 +03:00
Lifting (#2)
* Initial LoginStateMachine implementation * Nicer interface * Lifting instance for (->) and Identity, liftKleisli function * Added Control.Category.Lifting to free-algebras * Reoder Lifting module * Fixed haddoc documentation * examples.cabal - base version * reconfigure circle-ci * Fixed error in GHC-8.6.1
This commit is contained in:
parent
34d9b45c07
commit
62d0bbe4fe
@ -39,33 +39,53 @@ jobs:
|
||||
- setup
|
||||
- run:
|
||||
name: "GHC 861"
|
||||
command:
|
||||
nix-build --argstr compiler ghc861
|
||||
- cachix-push
|
||||
command: |
|
||||
nix-build -A free-category -o result-fc --argstr compiler ghc861
|
||||
nix-build -A examples -o result-ex --argstr compiler ghc861
|
||||
- cachix-push:
|
||||
o: result-fc
|
||||
- cachix-push:
|
||||
o: result-ex
|
||||
GHC844:
|
||||
<<: *defaults
|
||||
steps:
|
||||
- setup
|
||||
- run:
|
||||
name: "GHC 844"
|
||||
command: nix-build --argstr compiler ghc844
|
||||
- cachix-push
|
||||
command: |
|
||||
nix-build -A free-category -o result-fc --argstr compiler ghc844
|
||||
nix-build -A examples -o result-ex --argstr compiler ghc844
|
||||
- cachix-push:
|
||||
o: result-fc
|
||||
- cachix-push:
|
||||
o: result-ex
|
||||
GHC822:
|
||||
<<: *defaults
|
||||
steps:
|
||||
- setup
|
||||
- run:
|
||||
name: "GHC 822"
|
||||
command: nix-build --argstr compiler ghc822
|
||||
- cachix-push
|
||||
command: |
|
||||
nix-build -A free-category -o result-fc --argstr compiler ghc822
|
||||
nix-build -A examples -o result-ex --argstr compiler ghc822
|
||||
- cachix-push:
|
||||
o: result-fc
|
||||
- cachix-push:
|
||||
o: result-ex
|
||||
|
||||
GHC802:
|
||||
<<: *defaults
|
||||
steps:
|
||||
- setup
|
||||
- run:
|
||||
name: "GHC 802"
|
||||
command: nix-build --argstr compiler ghc802
|
||||
- cachix-push
|
||||
command: |
|
||||
nix-build -A free-category -o result-fc --argstr compiler ghc802
|
||||
nix-build -A examples -o result-ex --argstr compiler ghc802
|
||||
- cachix-push:
|
||||
o: result-fc
|
||||
- cachix-push:
|
||||
o: result-ex
|
||||
|
||||
workflows:
|
||||
build:
|
||||
|
2
cabal.project
Normal file
2
cabal.project
Normal file
@ -0,0 +1,2 @@
|
||||
packages: .
|
||||
./examples
|
@ -25,6 +25,10 @@ let
|
||||
else nixpkgs.lib.id;
|
||||
|
||||
free-category = doDev(doHaddock(doTest(doBench(
|
||||
pkgs.${compiler}.callPackage ./pkg.nix { inherit nixpkgs; }))));
|
||||
pkgs.${compiler}.callPackage ./pkg.nix
|
||||
{ inherit nixpkgs; }))));
|
||||
examples = doDev(doHaddock(doTest(doBench(
|
||||
pkgs.${compiler}.callPackage ./examples/pkg.nix
|
||||
{ inherit free-category nixpkgs; }))));
|
||||
in
|
||||
{ inherit free-category; }
|
||||
{ inherit free-category examples; }
|
||||
|
5
examples/CHANGELOG.md
Normal file
5
examples/CHANGELOG.md
Normal file
@ -0,0 +1,5 @@
|
||||
# Revision history for examples
|
||||
|
||||
## 0.1.0.0 -- YYYY-mm-dd
|
||||
|
||||
* First version. Released on an unsuspecting world.
|
373
examples/LICENSE
Normal file
373
examples/LICENSE
Normal file
@ -0,0 +1,373 @@
|
||||
Mozilla Public License Version 2.0
|
||||
==================================
|
||||
|
||||
1. Definitions
|
||||
--------------
|
||||
|
||||
1.1. "Contributor"
|
||||
means each individual or legal entity that creates, contributes to
|
||||
the creation of, or owns Covered Software.
|
||||
|
||||
1.2. "Contributor Version"
|
||||
means the combination of the Contributions of others (if any) used
|
||||
by a Contributor and that particular Contributor's Contribution.
|
||||
|
||||
1.3. "Contribution"
|
||||
means Covered Software of a particular Contributor.
|
||||
|
||||
1.4. "Covered Software"
|
||||
means Source Code Form to which the initial Contributor has attached
|
||||
the notice in Exhibit A, the Executable Form of such Source Code
|
||||
Form, and Modifications of such Source Code Form, in each case
|
||||
including portions thereof.
|
||||
|
||||
1.5. "Incompatible With Secondary Licenses"
|
||||
means
|
||||
|
||||
(a) that the initial Contributor has attached the notice described
|
||||
in Exhibit B to the Covered Software; or
|
||||
|
||||
(b) that the Covered Software was made available under the terms of
|
||||
version 1.1 or earlier of the License, but not also under the
|
||||
terms of a Secondary License.
|
||||
|
||||
1.6. "Executable Form"
|
||||
means any form of the work other than Source Code Form.
|
||||
|
||||
1.7. "Larger Work"
|
||||
means a work that combines Covered Software with other material, in
|
||||
a separate file or files, that is not Covered Software.
|
||||
|
||||
1.8. "License"
|
||||
means this document.
|
||||
|
||||
1.9. "Licensable"
|
||||
means having the right to grant, to the maximum extent possible,
|
||||
whether at the time of the initial grant or subsequently, any and
|
||||
all of the rights conveyed by this License.
|
||||
|
||||
1.10. "Modifications"
|
||||
means any of the following:
|
||||
|
||||
(a) any file in Source Code Form that results from an addition to,
|
||||
deletion from, or modification of the contents of Covered
|
||||
Software; or
|
||||
|
||||
(b) any new file in Source Code Form that contains any Covered
|
||||
Software.
|
||||
|
||||
1.11. "Patent Claims" of a Contributor
|
||||
means any patent claim(s), including without limitation, method,
|
||||
process, and apparatus claims, in any patent Licensable by such
|
||||
Contributor that would be infringed, but for the grant of the
|
||||
License, by the making, using, selling, offering for sale, having
|
||||
made, import, or transfer of either its Contributions or its
|
||||
Contributor Version.
|
||||
|
||||
1.12. "Secondary License"
|
||||
means either the GNU General Public License, Version 2.0, the GNU
|
||||
Lesser General Public License, Version 2.1, the GNU Affero General
|
||||
Public License, Version 3.0, or any later versions of those
|
||||
licenses.
|
||||
|
||||
1.13. "Source Code Form"
|
||||
means the form of the work preferred for making modifications.
|
||||
|
||||
1.14. "You" (or "Your")
|
||||
means an individual or a legal entity exercising rights under this
|
||||
License. For legal entities, "You" includes any entity that
|
||||
controls, is controlled by, or is under common control with You. For
|
||||
purposes of this definition, "control" means (a) the power, direct
|
||||
or indirect, to cause the direction or management of such entity,
|
||||
whether by contract or otherwise, or (b) ownership of more than
|
||||
fifty percent (50%) of the outstanding shares or beneficial
|
||||
ownership of such entity.
|
||||
|
||||
2. License Grants and Conditions
|
||||
--------------------------------
|
||||
|
||||
2.1. Grants
|
||||
|
||||
Each Contributor hereby grants You a world-wide, royalty-free,
|
||||
non-exclusive license:
|
||||
|
||||
(a) under intellectual property rights (other than patent or trademark)
|
||||
Licensable by such Contributor to use, reproduce, make available,
|
||||
modify, display, perform, distribute, and otherwise exploit its
|
||||
Contributions, either on an unmodified basis, with Modifications, or
|
||||
as part of a Larger Work; and
|
||||
|
||||
(b) under Patent Claims of such Contributor to make, use, sell, offer
|
||||
for sale, have made, import, and otherwise transfer either its
|
||||
Contributions or its Contributor Version.
|
||||
|
||||
2.2. Effective Date
|
||||
|
||||
The licenses granted in Section 2.1 with respect to any Contribution
|
||||
become effective for each Contribution on the date the Contributor first
|
||||
distributes such Contribution.
|
||||
|
||||
2.3. Limitations on Grant Scope
|
||||
|
||||
The licenses granted in this Section 2 are the only rights granted under
|
||||
this License. No additional rights or licenses will be implied from the
|
||||
distribution or licensing of Covered Software under this License.
|
||||
Notwithstanding Section 2.1(b) above, no patent license is granted by a
|
||||
Contributor:
|
||||
|
||||
(a) for any code that a Contributor has removed from Covered Software;
|
||||
or
|
||||
|
||||
(b) for infringements caused by: (i) Your and any other third party's
|
||||
modifications of Covered Software, or (ii) the combination of its
|
||||
Contributions with other software (except as part of its Contributor
|
||||
Version); or
|
||||
|
||||
(c) under Patent Claims infringed by Covered Software in the absence of
|
||||
its Contributions.
|
||||
|
||||
This License does not grant any rights in the trademarks, service marks,
|
||||
or logos of any Contributor (except as may be necessary to comply with
|
||||
the notice requirements in Section 3.4).
|
||||
|
||||
2.4. Subsequent Licenses
|
||||
|
||||
No Contributor makes additional grants as a result of Your choice to
|
||||
distribute the Covered Software under a subsequent version of this
|
||||
License (see Section 10.2) or under the terms of a Secondary License (if
|
||||
permitted under the terms of Section 3.3).
|
||||
|
||||
2.5. Representation
|
||||
|
||||
Each Contributor represents that the Contributor believes its
|
||||
Contributions are its original creation(s) or it has sufficient rights
|
||||
to grant the rights to its Contributions conveyed by this License.
|
||||
|
||||
2.6. Fair Use
|
||||
|
||||
This License is not intended to limit any rights You have under
|
||||
applicable copyright doctrines of fair use, fair dealing, or other
|
||||
equivalents.
|
||||
|
||||
2.7. Conditions
|
||||
|
||||
Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted
|
||||
in Section 2.1.
|
||||
|
||||
3. Responsibilities
|
||||
-------------------
|
||||
|
||||
3.1. Distribution of Source Form
|
||||
|
||||
All distribution of Covered Software in Source Code Form, including any
|
||||
Modifications that You create or to which You contribute, must be under
|
||||
the terms of this License. You must inform recipients that the Source
|
||||
Code Form of the Covered Software is governed by the terms of this
|
||||
License, and how they can obtain a copy of this License. You may not
|
||||
attempt to alter or restrict the recipients' rights in the Source Code
|
||||
Form.
|
||||
|
||||
3.2. Distribution of Executable Form
|
||||
|
||||
If You distribute Covered Software in Executable Form then:
|
||||
|
||||
(a) such Covered Software must also be made available in Source Code
|
||||
Form, as described in Section 3.1, and You must inform recipients of
|
||||
the Executable Form how they can obtain a copy of such Source Code
|
||||
Form by reasonable means in a timely manner, at a charge no more
|
||||
than the cost of distribution to the recipient; and
|
||||
|
||||
(b) You may distribute such Executable Form under the terms of this
|
||||
License, or sublicense it under different terms, provided that the
|
||||
license for the Executable Form does not attempt to limit or alter
|
||||
the recipients' rights in the Source Code Form under this License.
|
||||
|
||||
3.3. Distribution of a Larger Work
|
||||
|
||||
You may create and distribute a Larger Work under terms of Your choice,
|
||||
provided that You also comply with the requirements of this License for
|
||||
the Covered Software. If the Larger Work is a combination of Covered
|
||||
Software with a work governed by one or more Secondary Licenses, and the
|
||||
Covered Software is not Incompatible With Secondary Licenses, this
|
||||
License permits You to additionally distribute such Covered Software
|
||||
under the terms of such Secondary License(s), so that the recipient of
|
||||
the Larger Work may, at their option, further distribute the Covered
|
||||
Software under the terms of either this License or such Secondary
|
||||
License(s).
|
||||
|
||||
3.4. Notices
|
||||
|
||||
You may not remove or alter the substance of any license notices
|
||||
(including copyright notices, patent notices, disclaimers of warranty,
|
||||
or limitations of liability) contained within the Source Code Form of
|
||||
the Covered Software, except that You may alter any license notices to
|
||||
the extent required to remedy known factual inaccuracies.
|
||||
|
||||
3.5. Application of Additional Terms
|
||||
|
||||
You may choose to offer, and to charge a fee for, warranty, support,
|
||||
indemnity or liability obligations to one or more recipients of Covered
|
||||
Software. However, You may do so only on Your own behalf, and not on
|
||||
behalf of any Contributor. You must make it absolutely clear that any
|
||||
such warranty, support, indemnity, or liability obligation is offered by
|
||||
You alone, and You hereby agree to indemnify every Contributor for any
|
||||
liability incurred by such Contributor as a result of warranty, support,
|
||||
indemnity or liability terms You offer. You may include additional
|
||||
disclaimers of warranty and limitations of liability specific to any
|
||||
jurisdiction.
|
||||
|
||||
4. Inability to Comply Due to Statute or Regulation
|
||||
---------------------------------------------------
|
||||
|
||||
If it is impossible for You to comply with any of the terms of this
|
||||
License with respect to some or all of the Covered Software due to
|
||||
statute, judicial order, or regulation then You must: (a) comply with
|
||||
the terms of this License to the maximum extent possible; and (b)
|
||||
describe the limitations and the code they affect. Such description must
|
||||
be placed in a text file included with all distributions of the Covered
|
||||
Software under this License. Except to the extent prohibited by statute
|
||||
or regulation, such description must be sufficiently detailed for a
|
||||
recipient of ordinary skill to be able to understand it.
|
||||
|
||||
5. Termination
|
||||
--------------
|
||||
|
||||
5.1. The rights granted under this License will terminate automatically
|
||||
if You fail to comply with any of its terms. However, if You become
|
||||
compliant, then the rights granted under this License from a particular
|
||||
Contributor are reinstated (a) provisionally, unless and until such
|
||||
Contributor explicitly and finally terminates Your grants, and (b) on an
|
||||
ongoing basis, if such Contributor fails to notify You of the
|
||||
non-compliance by some reasonable means prior to 60 days after You have
|
||||
come back into compliance. Moreover, Your grants from a particular
|
||||
Contributor are reinstated on an ongoing basis if such Contributor
|
||||
notifies You of the non-compliance by some reasonable means, this is the
|
||||
first time You have received notice of non-compliance with this License
|
||||
from such Contributor, and You become compliant prior to 30 days after
|
||||
Your receipt of the notice.
|
||||
|
||||
5.2. If You initiate litigation against any entity by asserting a patent
|
||||
infringement claim (excluding declaratory judgment actions,
|
||||
counter-claims, and cross-claims) alleging that a Contributor Version
|
||||
directly or indirectly infringes any patent, then the rights granted to
|
||||
You by any and all Contributors for the Covered Software under Section
|
||||
2.1 of this License shall terminate.
|
||||
|
||||
5.3. In the event of termination under Sections 5.1 or 5.2 above, all
|
||||
end user license agreements (excluding distributors and resellers) which
|
||||
have been validly granted by You or Your distributors under this License
|
||||
prior to termination shall survive termination.
|
||||
|
||||
************************************************************************
|
||||
* *
|
||||
* 6. Disclaimer of Warranty *
|
||||
* ------------------------- *
|
||||
* *
|
||||
* Covered Software is provided under this License on an "as is" *
|
||||
* basis, without warranty of any kind, either expressed, implied, or *
|
||||
* statutory, including, without limitation, warranties that the *
|
||||
* Covered Software is free of defects, merchantable, fit for a *
|
||||
* particular purpose or non-infringing. The entire risk as to the *
|
||||
* quality and performance of the Covered Software is with You. *
|
||||
* Should any Covered Software prove defective in any respect, You *
|
||||
* (not any Contributor) assume the cost of any necessary servicing, *
|
||||
* repair, or correction. This disclaimer of warranty constitutes an *
|
||||
* essential part of this License. No use of any Covered Software is *
|
||||
* authorized under this License except under this disclaimer. *
|
||||
* *
|
||||
************************************************************************
|
||||
|
||||
************************************************************************
|
||||
* *
|
||||
* 7. Limitation of Liability *
|
||||
* -------------------------- *
|
||||
* *
|
||||
* Under no circumstances and under no legal theory, whether tort *
|
||||
* (including negligence), contract, or otherwise, shall any *
|
||||
* Contributor, or anyone who distributes Covered Software as *
|
||||
* permitted above, be liable to You for any direct, indirect, *
|
||||
* special, incidental, or consequential damages of any character *
|
||||
* including, without limitation, damages for lost profits, loss of *
|
||||
* goodwill, work stoppage, computer failure or malfunction, or any *
|
||||
* and all other commercial damages or losses, even if such party *
|
||||
* shall have been informed of the possibility of such damages. This *
|
||||
* limitation of liability shall not apply to liability for death or *
|
||||
* personal injury resulting from such party's negligence to the *
|
||||
* extent applicable law prohibits such limitation. Some *
|
||||
* jurisdictions do not allow the exclusion or limitation of *
|
||||
* incidental or consequential damages, so this exclusion and *
|
||||
* limitation may not apply to You. *
|
||||
* *
|
||||
************************************************************************
|
||||
|
||||
8. Litigation
|
||||
-------------
|
||||
|
||||
Any litigation relating to this License may be brought only in the
|
||||
courts of a jurisdiction where the defendant maintains its principal
|
||||
place of business and such litigation shall be governed by laws of that
|
||||
jurisdiction, without reference to its conflict-of-law provisions.
|
||||
Nothing in this Section shall prevent a party's ability to bring
|
||||
cross-claims or counter-claims.
|
||||
|
||||
9. Miscellaneous
|
||||
----------------
|
||||
|
||||
This License represents the complete agreement concerning the subject
|
||||
matter hereof. If any provision of this License is held to be
|
||||
unenforceable, such provision shall be reformed only to the extent
|
||||
necessary to make it enforceable. Any law or regulation which provides
|
||||
that the language of a contract shall be construed against the drafter
|
||||
shall not be used to construe this License against a Contributor.
|
||||
|
||||
10. Versions of the License
|
||||
---------------------------
|
||||
|
||||
10.1. New Versions
|
||||
|
||||
Mozilla Foundation is the license steward. Except as provided in Section
|
||||
10.3, no one other than the license steward has the right to modify or
|
||||
publish new versions of this License. Each version will be given a
|
||||
distinguishing version number.
|
||||
|
||||
10.2. Effect of New Versions
|
||||
|
||||
You may distribute the Covered Software under the terms of the version
|
||||
of the License under which You originally received the Covered Software,
|
||||
or under the terms of any subsequent version published by the license
|
||||
steward.
|
||||
|
||||
10.3. Modified Versions
|
||||
|
||||
If you create software not governed by this License, and you want to
|
||||
create a new license for such software, you may create and use a
|
||||
modified version of this License if you rename the license and remove
|
||||
any references to the name of the license steward (except to note that
|
||||
such modified license differs from this License).
|
||||
|
||||
10.4. Distributing Source Code Form that is Incompatible With Secondary
|
||||
Licenses
|
||||
|
||||
If You choose to distribute Source Code Form that is Incompatible With
|
||||
Secondary Licenses under the terms of this version of the License, the
|
||||
notice described in Exhibit B of this License must be attached.
|
||||
|
||||
Exhibit A - Source Code Form License Notice
|
||||
-------------------------------------------
|
||||
|
||||
This Source Code Form is subject to the terms of the Mozilla Public
|
||||
License, v. 2.0. If a copy of the MPL was not distributed with this
|
||||
file, You can obtain one at http://mozilla.org/MPL/2.0/.
|
||||
|
||||
If it is not possible or desirable to put the notice in a particular
|
||||
file, then You may include the notice in a location (such as a LICENSE
|
||||
file in a relevant directory) where a recipient would be likely to look
|
||||
for such a notice.
|
||||
|
||||
You may add additional accurate notices of copyright ownership.
|
||||
|
||||
Exhibit B - "Incompatible With Secondary Licenses" Notice
|
||||
---------------------------------------------------------
|
||||
|
||||
This Source Code Form is "Incompatible With Secondary Licenses", as
|
||||
defined by the Mozilla Public License, v. 2.0.
|
2
examples/Setup.hs
Normal file
2
examples/Setup.hs
Normal file
@ -0,0 +1,2 @@
|
||||
import Distribution.Simple
|
||||
main = defaultMain
|
31
examples/examples.cabal
Normal file
31
examples/examples.cabal
Normal file
@ -0,0 +1,31 @@
|
||||
-- Initial examples.cabal generated by cabal init. For further
|
||||
-- documentation, see http://haskell.org/cabal/users-guide/
|
||||
|
||||
name: examples
|
||||
version: 0.1.0.0
|
||||
-- synopsis:
|
||||
-- description:
|
||||
license: MPL-2.0
|
||||
license-file: LICENSE
|
||||
author: Marcin Szamotulski
|
||||
maintainer: profunctor@pm.me
|
||||
-- copyright:
|
||||
-- category:
|
||||
build-type: Simple
|
||||
extra-source-files: CHANGELOG.md
|
||||
cabal-version: >=1.10
|
||||
|
||||
library
|
||||
exposed-modules: LoginStateMachine
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
build-depends: base >=4.9 && <5
|
||||
, free-category >= 0.0.1.0
|
||||
, free-algebras >= 0.0.7.0
|
||||
hs-source-dirs: src
|
||||
default-language: Haskell2010
|
||||
ghc-options: -Wall
|
||||
-fwarn-incomplete-record-updates
|
||||
-fwarn-incomplete-uni-patterns
|
||||
-fwarn-redundant-constraints
|
||||
-fwarn-deprecations
|
21
examples/pkg.nix
Normal file
21
examples/pkg.nix
Normal file
@ -0,0 +1,21 @@
|
||||
{ nixpkgs
|
||||
, mkDerivation
|
||||
, base
|
||||
, free-category
|
||||
, free-algebras
|
||||
, stdenv
|
||||
}:
|
||||
mkDerivation {
|
||||
pname = "free-category-examples";
|
||||
version = "0.0.1.0";
|
||||
src = nixpkgs.lib.sourceFilesBySuffices ./.
|
||||
[ ".hs" "LICENSE" "ChangeLog.md" "examples.cabal" ];
|
||||
libraryHaskellDepends = [
|
||||
base
|
||||
free-category
|
||||
free-algebras
|
||||
];
|
||||
libraryToolDepends = [ ];
|
||||
license = stdenv.lib.licenses.mpl20;
|
||||
enableSeparateDocOutput = false;
|
||||
}
|
163
examples/src/LoginStateMachine.hs
Normal file
163
examples/src/LoginStateMachine.hs
Normal file
@ -0,0 +1,163 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module LoginStateMachine where
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Arrow (Kleisli (..))
|
||||
import Control.Category (Category (..))
|
||||
|
||||
import Control.Category.Free (Cat)
|
||||
|
||||
-- Import classes and combintators used in this example
|
||||
import Control.Category.Lifting
|
||||
|
||||
{-------------------------------------------------------------------------------
|
||||
-- Example State Machine, inspired by:
|
||||
-- `State Machines All The Way Down` by Edwin Bradly, 2017
|
||||
-- https://www.youtube.com/watch?v=xq7ZuSRgCR4
|
||||
-------------------------------------------------------------------------------}
|
||||
|
||||
data LoginResult = Success | LoginError
|
||||
|
||||
-- | Type level representation of the states.
|
||||
--
|
||||
data StateType where
|
||||
LoggedInType :: StateType
|
||||
LoggedOutType :: StateType
|
||||
|
||||
data SStateType (a :: StateType) where
|
||||
SLoggedIn :: SStateType 'LoggedInType
|
||||
SLoggedOut :: SStateType 'LoggedOutType
|
||||
|
||||
-- | Term level representation of the states.
|
||||
-- @'LoggedOut'@ let one carry out a value.
|
||||
--
|
||||
data State a (st :: StateType) where
|
||||
LoggedIn :: State a 'LoggedInType
|
||||
LoggedOut :: Maybe a -> State a 'LoggedOutType
|
||||
|
||||
runLoggedOut :: State a 'LoggedOutType -> Maybe a
|
||||
runLoggedOut (LoggedOut a) = a
|
||||
|
||||
-- | Graph of transitions in the state machine.
|
||||
-- In abstract representation the states do not show up, the only way to record
|
||||
-- some data is to addit to the transition. Thus @'Logout'@ can carry data.
|
||||
-- When interpreted in a some category (e.g. @'Kleisli' m@) then the data will
|
||||
-- be avalable on @'LoggedOut{} :: 'State' a st@.
|
||||
data Tr a from to where
|
||||
Login :: SStateType to -> Tr a (State a 'LoggedOutType) (State a to)
|
||||
Logout :: Maybe a -> Tr a (State a 'LoggedInType) (State a 'LoggedOutType)
|
||||
Access :: Tr a (State a 'LoggedInType) (State a 'LoggedInType)
|
||||
|
||||
login :: Monad m
|
||||
=> SStateType st
|
||||
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedOutType) (State a st)
|
||||
login = liftCat . Login
|
||||
|
||||
logout :: Monad m
|
||||
=> Maybe a
|
||||
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
|
||||
logout = liftCat . Logout
|
||||
|
||||
access :: Monad m
|
||||
=> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedInType)
|
||||
access = liftCat Access
|
||||
|
||||
type Username = String
|
||||
|
||||
-- * Data representation of the state machine.
|
||||
|
||||
newtype HandleLogin m authToken a = HandleLogin {
|
||||
handleLogin :: authToken -> m (Maybe (HandleAccess m a))
|
||||
}
|
||||
|
||||
data HandleAccess m a where
|
||||
AccessHandler
|
||||
:: m a -- access secret
|
||||
-> (a -> m (HandleAccess m a)) -- handle secret
|
||||
-> HandleAccess m a
|
||||
LogoutHandler :: HandleAccess m a
|
||||
|
||||
exampleHandleLogin
|
||||
:: Applicative m
|
||||
=> String
|
||||
-> HandleLogin m String String
|
||||
exampleHandleLogin passwd = HandleLogin $ \authToken ->
|
||||
if authToken == passwd
|
||||
then pure (Just handleAccess)
|
||||
else pure Nothing
|
||||
where
|
||||
handleAccess = AccessHandler (pure "secret") (\_ -> pure LogoutHandler)
|
||||
|
||||
|
||||
-- * Abstract access function, also an isomorphism between @'HandleLogin' m a@
|
||||
-- and @'FreeLifting m (Tr a) (State a 'LoggedoutType) (State
|
||||
-- a 'LoggedOutType).
|
||||
|
||||
accessSecret
|
||||
:: forall m authToken a. Monad m
|
||||
=> authToken
|
||||
-> HandleLogin m authToken a
|
||||
-> FreeLifting m (Cat (Tr a)) (State a 'LoggedOutType) (State a 'LoggedOutType)
|
||||
accessSecret authToken HandleLogin{handleLogin} = lift $ do
|
||||
st <- handleLogin authToken
|
||||
case st of
|
||||
Just accessHandler -> return $ handle accessHandler Nothing . login SLoggedIn
|
||||
Nothing -> return id
|
||||
where
|
||||
handle :: HandleAccess m a -> Maybe a -> FreeLifting m (Cat (Tr a)) (State a 'LoggedInType) (State a 'LoggedOutType)
|
||||
handle LogoutHandler ma = logout ma
|
||||
handle (AccessHandler accessHandler dataHandler) _ = lift $ do
|
||||
a <- accessHandler
|
||||
accessHandler' <- dataHandler a
|
||||
return $ handle accessHandler' (Just a)
|
||||
|
||||
-- | Get data following the protocol defined by the state machine.
|
||||
--
|
||||
-- Note: in GHC-8.6.1 we'd need @'MonadFail'@ which prevents from running this in
|
||||
-- @'Identity'@ monad. To avoid this we use @'runLoggedOut'@ function.
|
||||
getData
|
||||
:: forall m authToken a.
|
||||
( Monad m )
|
||||
=> (forall x y. Tr a x y -> Kleisli m x y)
|
||||
-> HandleLogin m authToken a
|
||||
-> authToken
|
||||
-> m (Maybe a)
|
||||
getData nat handleLogin authToken = case foldNatLift nat (accessSecret authToken handleLogin) of
|
||||
Kleisli fn -> do
|
||||
ma <- runLoggedOut <$> fn (LoggedOut Nothing)
|
||||
return ma
|
||||
|
||||
-- * Interpreters
|
||||
-- To write an interpret it is enough to supply a natural transformation from
|
||||
-- @'Tr' a from to@ to @'Kleisli' m@ for some monad @m@.
|
||||
|
||||
-- | A pure natural transformation from @'Tr'@ to @'Kleisli' m@ for some
|
||||
-- @'Monad' m@. Note, that even though @'Kleisli'@ category seems redundant
|
||||
-- here, as we don't use the monad in the transformation, we need
|
||||
-- a transformation into a category that satisfies the @'Lifing'@ constraint.
|
||||
-- This is bause we will need the monad whn @'foldNatLift'@ will walk over the
|
||||
-- constructors of '@FreeLifting'@ category.
|
||||
--
|
||||
natPure :: forall m a from to. Monad m => Tr a from to -> Kleisli m from to
|
||||
natPure = liftKleisli . nat
|
||||
where
|
||||
-- a natural trasformation to @'->'@
|
||||
nat :: Tr a from to -> (from -> to)
|
||||
nat (Login SLoggedIn) = \_ -> LoggedIn
|
||||
nat (Login SLoggedOut) = \_ -> (LoggedOut Nothing)
|
||||
nat (Logout ma) = \_ -> (LoggedOut ma)
|
||||
nat Access = \_ -> LoggedIn
|
||||
|
||||
-- | A trivial program, which extracts a trivial secret.
|
||||
main :: IO ()
|
||||
main = do
|
||||
putStrLn "Provide a password:"
|
||||
authToken <- getLine
|
||||
secret <- getData natPure (exampleHandleLogin "password") authToken
|
||||
putStrLn ("Secret: " ++ show secret)
|
@ -24,31 +24,32 @@ library
|
||||
exposed-modules:
|
||||
Control.Arrow.Free
|
||||
Control.Category.Free
|
||||
Control.Category.Lifting
|
||||
other-modules:
|
||||
Paths_free_category
|
||||
hs-source-dirs:
|
||||
src
|
||||
default-extensions:
|
||||
ConstraintKinds
|
||||
DataKinds
|
||||
DeriveFunctor
|
||||
EmptyDataDecls
|
||||
FlexibleInstances
|
||||
FlexibleContexts
|
||||
GADTs
|
||||
KindSignatures
|
||||
InstanceSigs
|
||||
MultiParamTypeClasses
|
||||
OverloadedStrings
|
||||
PolyKinds
|
||||
RankNTypes
|
||||
ScopedTypeVariables
|
||||
TupleSections
|
||||
TypeApplications
|
||||
TypeFamilies
|
||||
ConstraintKinds
|
||||
DataKinds
|
||||
DeriveFunctor
|
||||
EmptyDataDecls
|
||||
FlexibleInstances
|
||||
FlexibleContexts
|
||||
GADTs
|
||||
KindSignatures
|
||||
InstanceSigs
|
||||
MultiParamTypeClasses
|
||||
OverloadedStrings
|
||||
PolyKinds
|
||||
RankNTypes
|
||||
ScopedTypeVariables
|
||||
TupleSections
|
||||
TypeApplications
|
||||
TypeFamilies
|
||||
build-depends:
|
||||
base >= 4.9 && <5
|
||||
, free-algebras >= 0.0.6.0
|
||||
, free-algebras >= 0.0.7.0
|
||||
ghc-options:
|
||||
-Wall
|
||||
-fwarn-incomplete-record-updates
|
||||
|
@ -4,8 +4,8 @@
|
||||
}:
|
||||
mkDerivation {
|
||||
pname = "free-algebras";
|
||||
version = "0.0.6.0";
|
||||
sha256 = "5a1d919b76fbe8697fae4c8d79ade62f9616ae44a1fa330aff415f352857628c";
|
||||
version = "0.0.7.0";
|
||||
sha256 = "f0c18b857087ec7ec0321f729562174c9a9f02172806e2fba7c8989fdd7631aa";
|
||||
libraryHaskellDepends = [
|
||||
base constraints containers data-fix dlist free groups
|
||||
kan-extensions mtl natural-numbers transformers
|
||||
|
@ -1,4 +1,4 @@
|
||||
{ compiler ? "ghc843"
|
||||
{ compiler ? "ghc844"
|
||||
, haddock ? true
|
||||
, test ? true
|
||||
, benchmarks ? false
|
||||
@ -13,4 +13,7 @@ in
|
||||
free-category = if nixpkgs.lib.inNixShell
|
||||
then default.free-category.env
|
||||
else default.free-category;
|
||||
examples = if nixpkgs.lib.inNixShell
|
||||
then default.examples.env
|
||||
else default.examples;
|
||||
}
|
||||
|
@ -37,8 +37,6 @@ import Control.Arrow (Arrow (..), ArrowZero (..), ArrowChoice (..))
|
||||
import Data.Monoid (Monoid (..))
|
||||
import Data.Semigroup (Semigroup (..))
|
||||
#endif
|
||||
import Data.Monoid.MSet (MSet (..))
|
||||
import Data.Semigroup.SSet (SSet (..))
|
||||
|
||||
-- |
|
||||
-- Free category encoded as a recursive data type, in a simlar way as
|
||||
@ -49,7 +47,7 @@ import Data.Semigroup.SSet (SSet (..))
|
||||
--
|
||||
-- The same performance concerns that apply to @'Control.Monad.Free.Free'@
|
||||
-- apply to this encoding of a free category.
|
||||
data Cat :: (* -> * -> *) -> * -> * -> * where
|
||||
data Cat :: (k -> k -> *) -> k -> k -> * where
|
||||
Id :: Cat f a a
|
||||
(:.:) :: f b c -> Cat f a b -> Cat f a c
|
||||
|
||||
@ -86,14 +84,6 @@ instance Monoid (Cat f o o) where
|
||||
mappend = (<>)
|
||||
#endif
|
||||
|
||||
instance SSet (Cat f o o) (Cat f a o) where
|
||||
act = (.)
|
||||
|
||||
instance MSet (Cat f o o) (Cat f a o) where
|
||||
#if __GLASGOW_HASKELL__ < 804
|
||||
mact = (.)
|
||||
#endif
|
||||
|
||||
type instance AlgebraType0 Cat f = ()
|
||||
type instance AlgebraType Cat c = Category c
|
||||
|
||||
@ -168,11 +158,3 @@ instance Monoid (C f o o) where
|
||||
#if __GLASGOW_HASKELL__ < 804
|
||||
mappend = (<>)
|
||||
#endif
|
||||
|
||||
instance SSet (C f o o) (C f a o) where
|
||||
act = (.)
|
||||
|
||||
instance MSet (C f o o) (C f a o) where
|
||||
#if __GLASGOW_HASKELL__ < 804
|
||||
mact = (.)
|
||||
#endif
|
||||
|
79
src/Control/Category/Lifting.hs
Normal file
79
src/Control/Category/Lifting.hs
Normal file
@ -0,0 +1,79 @@
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
module Control.Category.Lifting
|
||||
( Lifting (..)
|
||||
, FreeLifting (..)
|
||||
, liftCat
|
||||
, foldNatLift
|
||||
, liftKleisli
|
||||
) where
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Arrow (Kleisli (..))
|
||||
import Control.Category (Category (..))
|
||||
import Data.Functor.Identity (Identity (..))
|
||||
|
||||
import Control.Category.Free (Cat (..))
|
||||
import Control.Algebra.Free2 (FreeAlgebra2 (..))
|
||||
import Data.Algebra.Free (AlgebraType, AlgebraType0, proof)
|
||||
|
||||
-- | Categories which can lift monadic actions.
|
||||
--
|
||||
class Category c => Lifting c m | c -> m where
|
||||
lift :: m (c a b) -> c a b
|
||||
|
||||
instance Monad m => Lifting (Kleisli m) m where
|
||||
lift m = Kleisli (\a -> m >>= \(Kleisli f) -> f a)
|
||||
|
||||
instance Lifting (->) Identity where
|
||||
lift = runIdentity
|
||||
|
||||
-- | Category transformer, which adds @'Lifting'@ instance to the underlying
|
||||
-- base category.
|
||||
data FreeLifting :: (* -> *) -> (k -> k -> *) -> k -> k -> * where
|
||||
Base :: c a b -> FreeLifting m c a b
|
||||
Lift :: m (FreeLifting m c a b) -> FreeLifting m c a b
|
||||
|
||||
instance (Functor m, Category c) => Category (FreeLifting m c) where
|
||||
id = Base id
|
||||
Base f . Base g = Base $ f . g
|
||||
f . Lift mg = Lift $ (f .) <$> mg
|
||||
Lift mf . g = Lift $ (. g) <$> mf
|
||||
|
||||
instance (Functor m, Category c) => Lifting (FreeLifting m c) m where
|
||||
lift = Lift
|
||||
|
||||
type instance AlgebraType0 (FreeLifting m) c = (Monad m, Category c)
|
||||
type instance AlgebraType (FreeLifting m) c = Lifting c m
|
||||
instance Monad m => FreeAlgebra2 (FreeLifting m) where
|
||||
liftFree2 = Base
|
||||
foldNatFree2 nat (Base cab) = nat cab
|
||||
foldNatFree2 nat (Lift mcab) = lift $ foldNatFree2 nat <$> mcab
|
||||
|
||||
codom2 = proof
|
||||
forget2 = proof
|
||||
|
||||
-- | Wrap a transition into a free category @'Cat'@ and then in
|
||||
-- @'FreeLifting'@
|
||||
--
|
||||
-- prop> liftCat tr = Base (tr :.: Id)
|
||||
--
|
||||
liftCat :: Monad m => tr a b -> FreeLifting m (Cat tr) a b
|
||||
liftCat = liftFree2 . liftFree2
|
||||
|
||||
-- | Fold @'FreeLifing'@ category based on a free category @'Cat' tr@ using
|
||||
-- a functor @tr x y -> c x y@.
|
||||
--
|
||||
foldNatLift
|
||||
:: (Monad m, Lifting c m)
|
||||
=> (forall x y. tr x y -> c x y)
|
||||
-> FreeLifting m (Cat tr) a b
|
||||
-> c a b
|
||||
foldNatLift nat = foldNatFree2 (foldNatFree2 nat)
|
||||
|
||||
-- | Functor from @'->'@ category to @'Kleisli' m@. If @m@ is @Identity@ then
|
||||
-- it will respect @'lift'@ i.e. @lfitKleisli (lift ar) = lift (liftKleisli <$>
|
||||
-- ar).
|
||||
--
|
||||
liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b
|
||||
liftKleisli f = Kleisli (pure . f)
|
Loading…
Reference in New Issue
Block a user