mirror of
https://github.com/Jaxan/ons-hs.git
synced 2025-04-27 14:47:45 +02:00
More haddock documentation
This commit is contained in:
parent
83f6025acf
commit
41fbe68fbc
3 changed files with 97 additions and 27 deletions
|
@ -9,6 +9,9 @@ module Nominal (
|
||||||
-- | Re-exports from "Nominal.Support".
|
-- | Re-exports from "Nominal.Support".
|
||||||
Support,
|
Support,
|
||||||
-- * The Nominal type class
|
-- * The Nominal type class
|
||||||
|
-- | Re-exports from "Nominal.Class". Both trivial and generic instances can
|
||||||
|
-- be derived (via 'Trivially' and 'Generically'). For information on how to
|
||||||
|
-- derive instances for the type class, go to "Nominal.Class".
|
||||||
Nominal (..),
|
Nominal (..),
|
||||||
Trivially (..),
|
Trivially (..),
|
||||||
Generically (..),
|
Generically (..),
|
||||||
|
|
|
@ -23,3 +23,20 @@ newtype Atom = Atom {unAtom :: Int}
|
||||||
-- | Creates an atom with the value specified by the integer.
|
-- | Creates an atom with the value specified by the integer.
|
||||||
atom :: Int -> Atom
|
atom :: Int -> Atom
|
||||||
atom = Atom
|
atom = Atom
|
||||||
|
|
||||||
|
{- Notes:
|
||||||
|
|
||||||
|
- This type originally started out as Haskell's 'Rational' type. But since
|
||||||
|
all representatives would be computed by the library (e.g., in
|
||||||
|
'EquivariantSet'), the chosen atoms were always integers. Even in the
|
||||||
|
applications, such as automata learning, it is always possible to chose
|
||||||
|
integers. For that reason, the type is changed to 'Int'.
|
||||||
|
|
||||||
|
- The change from 'Rational' (which is 'Ration Integer', so a big number
|
||||||
|
type) to 'Int' did increase performance a little bit, around 5%. I guess
|
||||||
|
it also reduces the memory footprint, but I have not measured this.
|
||||||
|
|
||||||
|
- Most of the computations work on 'Orbit's anyways, and do not require
|
||||||
|
any representatives.
|
||||||
|
|
||||||
|
-}
|
||||||
|
|
|
@ -7,12 +7,19 @@
|
||||||
{-# LANGUAGE TypeOperators #-}
|
{-# LANGUAGE TypeOperators #-}
|
||||||
{-# LANGUAGE UndecidableInstances #-}
|
{-# LANGUAGE UndecidableInstances #-}
|
||||||
|
|
||||||
module Nominal.Class
|
module Nominal.Class (
|
||||||
( Nominal(..) -- typeclass
|
-- * Nominal
|
||||||
, Trivially(..) -- newtype wrapper for deriving instances
|
-- $Nominal
|
||||||
, Generically(..) -- newtype wrapper for deriving instances
|
Nominal(..),
|
||||||
, OrbPair(..) -- need to export?
|
-- ** Deriving trivial instances
|
||||||
, OrbRec(..) -- need to export?
|
-- $Trivial
|
||||||
|
Trivially(..),
|
||||||
|
-- ** Deriving generic instances
|
||||||
|
-- $Generic
|
||||||
|
Generically(..),
|
||||||
|
-- ** Implementation details
|
||||||
|
OrbPair(..),
|
||||||
|
OrbRec(..),
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Data.Kind (Type)
|
import Data.Kind (Type)
|
||||||
|
@ -23,29 +30,56 @@ import GHC.Generics
|
||||||
import Nominal.Atom
|
import Nominal.Atom
|
||||||
import Nominal.Support as Support
|
import Nominal.Support as Support
|
||||||
|
|
||||||
|
-- $Nominal
|
||||||
|
-- The type of nominal sets here is sometimes referred to as the "total
|
||||||
|
-- order symmetry", or "ordered atoms". The nominal sets in this setting are
|
||||||
|
-- always "strong", meaning that there are no "local symmetries".
|
||||||
|
--
|
||||||
|
-- References:
|
||||||
|
--
|
||||||
|
-- * <https://arxiv.org/abs/1402.0897v2>
|
||||||
|
-- * <https://arxiv.org/abs/1902.08414>
|
||||||
|
|
||||||
-- This is the main meat of the package. The Nominal typeclass, it gives us ways
|
-- | The Nominal typeclass gives us ways to manipulate nominal elements in sets
|
||||||
-- to manipulate nominal elements in sets and maps. The type class has
|
-- and maps. The type class has an associated type to represent orbits of type
|
||||||
-- associated data to represent an orbit of type a. This is often much easier
|
-- @a@. This type @'Orbit' a@ is often much simpler than the type @a@ itself.
|
||||||
-- than the type a itself. For example, all orbits of Rat are equal.
|
-- For example, all orbits of 'Atom' are equal (because the set of atoms is a
|
||||||
-- Furthermore, we provide means to go back and forth between elements and
|
-- single orbit).
|
||||||
|
--
|
||||||
|
-- The type class provides means to go back and forth between elements and
|
||||||
-- orbits, and we get to know their support size. For many manipulations we
|
-- orbits, and we get to know their support size. For many manipulations we
|
||||||
-- need an Ord instance on the associated data type, this can often be
|
-- need an 'Ord' instance on the associated data type, this can often be
|
||||||
-- implemented, even when the type 'a' does not have an Ord instance.
|
-- implemented, even when the type @a@ does not have an 'Ord' instance.
|
||||||
|
--
|
||||||
|
-- There are two ways to derive instances for this class, via 'Trivially' or
|
||||||
|
-- via 'Generically'. See below.
|
||||||
--
|
--
|
||||||
-- Laws / conditions:
|
-- Laws / conditions:
|
||||||
-- * index . toOrbit == size . support
|
--
|
||||||
-- * getElement o s is defined if index o == Set.size s
|
-- - 1. @index . toOrbit == size . support@
|
||||||
|
-- - 2. @toOrbit (getElement o supp) = o@ (if @supp@ has the right size)
|
||||||
|
-- - 3. @getElement (toOrbit a) (support a) = a@
|
||||||
class Nominal a where
|
class Nominal a where
|
||||||
|
-- | The type describing an orbit of type @a@.
|
||||||
type Orbit a :: Type
|
type Orbit a :: Type
|
||||||
|
|
||||||
|
-- | Maps an element to its orbit representation. In general, this maps
|
||||||
|
-- loses information about the input (namely the support).
|
||||||
toOrbit :: a -> Orbit a
|
toOrbit :: a -> Orbit a
|
||||||
|
|
||||||
|
-- | Returns the least support of an element.
|
||||||
support :: a -> Support
|
support :: a -> Support
|
||||||
|
|
||||||
|
-- | Picks an element from the orbit with a given support.
|
||||||
getElement :: Orbit a -> Support -> a
|
getElement :: Orbit a -> Support -> a
|
||||||
|
|
||||||
|
-- | The "atom dimension" of an orbit, it is the size of the support of any
|
||||||
|
-- of its elements.
|
||||||
index :: Proxy a -> Orbit a -> Int
|
index :: Proxy a -> Orbit a -> Int
|
||||||
|
|
||||||
|
|
||||||
-- We can construct orbits from rational numbers. There is exactly one orbit,
|
-- | The set of atoms consist of exactly one orbit. So the associated type
|
||||||
-- so this can be represented by the unit type.
|
-- is @()@.
|
||||||
instance Nominal Atom where
|
instance Nominal Atom where
|
||||||
type Orbit Atom = ()
|
type Orbit Atom = ()
|
||||||
toOrbit _ = ()
|
toOrbit _ = ()
|
||||||
|
@ -54,11 +88,11 @@ instance Nominal Atom where
|
||||||
index _ _ = 1
|
index _ _ = 1
|
||||||
|
|
||||||
|
|
||||||
-- Supports themselves are nominal. Note that this is a very important instance
|
-- 'Support's themselves are nominal. Note that this is a very important
|
||||||
-- as all other instances can reduce to this one (and perhaps the one for
|
-- instance as all other instances can reduce to this one (and perhaps the one
|
||||||
-- products). 'Abstract types' in the original ONS library can be represented
|
-- for products). "Abstract types" in the original ONS (C++) library can be
|
||||||
-- directly as T = (Trivial Int, Support). The orbit of a given support is
|
-- represented directly as @T = ('Int', 'Support')@. The orbit of a given
|
||||||
-- completely specified by an integer.
|
-- support is completely specified by an integer (representing the size).
|
||||||
instance Nominal Support where
|
instance Nominal Support where
|
||||||
type Orbit Support = Int
|
type Orbit Support = Int
|
||||||
toOrbit s = Support.size s
|
toOrbit s = Support.size s
|
||||||
|
@ -67,16 +101,28 @@ instance Nominal Support where
|
||||||
index _ n = n
|
index _ n = n
|
||||||
|
|
||||||
|
|
||||||
|
-- $Trivial
|
||||||
-- Two general ways for deriving instances are provided:
|
-- Two general ways for deriving instances are provided:
|
||||||
|
--
|
||||||
-- 1. A trivial instance, where the group action is trivial. This means that
|
-- 1. A trivial instance, where the group action is trivial. This means that
|
||||||
-- each value is its own orbit and is supported by the empty set.
|
-- each value is its own orbit and is supported by the empty set.
|
||||||
-- 2. A generic instance, this uses the GHC.Generis machinery. This will
|
--
|
||||||
-- derive ``the right'' instance based on the algebraic data type.
|
-- 2. A generic instance, this uses the "GHC.Generis" machinery. This will
|
||||||
-- Neither of them is a default, so they should be derived using DerivingVia.
|
-- derive the right instance based on the algebraic data type.
|
||||||
|
--
|
||||||
|
-- Neither of them is a default, so they should be derived using @DerivingVia@.
|
||||||
-- (Available from GHC 8.6.1.)
|
-- (Available from GHC 8.6.1.)
|
||||||
|
|
||||||
-- For the trivial action, each element is its own orbit and is supported
|
-- | For the trivial action, each element is its own orbit and is supported
|
||||||
-- by the empty set.
|
-- by the empty set. Use this as follows:
|
||||||
|
--
|
||||||
|
-- @
|
||||||
|
-- {-# LANGUAGE DerivingVia, StandaloneDeriving #-}
|
||||||
|
-- import GHC.Generics
|
||||||
|
-- data Colour = Red | Blue | Green
|
||||||
|
--
|
||||||
|
-- deriving via Trivially MyType instance Nominal MyType
|
||||||
|
-- @
|
||||||
newtype Trivially a = Trivial a
|
newtype Trivially a = Trivial a
|
||||||
instance Nominal (Trivially a) where
|
instance Nominal (Trivially a) where
|
||||||
type Orbit (Trivially a) = a
|
type Orbit (Trivially a) = a
|
||||||
|
@ -96,6 +142,10 @@ deriving via Trivially Int instance Nominal Int -- NB: Trivial instance!
|
||||||
deriving via Trivially Ordering instance Nominal Ordering
|
deriving via Trivially Ordering instance Nominal Ordering
|
||||||
|
|
||||||
|
|
||||||
|
-- $Generic
|
||||||
|
-- For deriving generically, use the 'Generically'. For convenience, this
|
||||||
|
-- helper type is re-exported from "GHC.Generics".
|
||||||
|
|
||||||
-- The generic instance unfolds the algebraic data type in sums and products,
|
-- The generic instance unfolds the algebraic data type in sums and products,
|
||||||
-- these have their own instances defined below.
|
-- these have their own instances defined below.
|
||||||
instance (Generic a, GNominal (Rep a)) => Nominal (Generically a) where
|
instance (Generic a, GNominal (Rep a)) => Nominal (Generically a) where
|
||||||
|
|
Loading…
Add table
Reference in a new issue