{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-
 - Copyright (C) 2020  Koz Ross <koz.ross@retro-freedom.nz>
 -
 - This program is free software: you can redistribute it and/or modify
 - it under the terms of the GNU General Public License as published by
 - the Free Software Foundation, either version 3 of the License, or
 - (at your option) any later version.
 -
 - This program is distributed in the hope that it will be useful,
 - but WITHOUT ANY WARRANTY; without even the implied warranty of
 - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 - GNU General Public License for more details.
 -
 - You should have received a copy of the GNU General Public License
 - along with this program.  If not, see <http://www.gnu.org/licenses/>.
 -}

-- |
-- Module: Data.Finitary.Optics
-- Description: Prisms and Isos for finitary types.
-- Copyright: (C) Koz Ross 2020
-- License: GPL version 3.0 or later
-- Maintainer: koz.ross@retro-freedom.nz
-- Stability: Experimental
-- Portability: GHC only
module Data.Finitary.Optics where

import Data.Finitary (Finitary (..))
import Data.Finite (strengthenN, weakenN)
import GHC.TypeNats (type (<=))
import Optics.Iso (Iso', iso)
import Optics.Prism (Prism', prism')

-- | Types with identical cardinalities can be freely interconverted by way of
-- their indexes.
--
-- This is actually stronger than most 'Iso's, as it also ensures that order is
-- preserved; namely, if @x < y@, then @view reindexed x < view reindexed y@.
reindexed :: (Finitary a, Finitary b, Cardinality a ~ Cardinality b) => Iso' a b
reindexed :: Iso' a b
reindexed = (a -> b) -> (b -> a) -> Iso' a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (Finite (Cardinality b) -> b
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality b) -> b)
-> (a -> Finite (Cardinality b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality b)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite) (Finite (Cardinality b) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality b) -> a)
-> (b -> Finite (Cardinality b)) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Finite (Cardinality b)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite)

-- | We can use indexes to convert a \'larger\' type to a smaller one, and
-- (possibly) vice-versa.
--
-- This is actually stronger than most 'Prism's, as it also ensures that order
-- is preserved in both directions. Specifically, if @x < y@, then:
--
-- * @review tighter x < review tighter y@; and
-- * If @preview tighter x == Just x'@ and @preview tighter y == Just y'@, then
-- @x' < y'@.
tighter :: (Finitary a, Finitary b, Cardinality b <= Cardinality a) => Prism' a b
tighter :: Prism' a b
tighter =
  (b -> a) -> (a -> Maybe b) -> Prism' a b
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a)
-> (b -> Finite (Cardinality a)) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality b) -> Finite (Cardinality a)
forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN (Finite (Cardinality b) -> Finite (Cardinality a))
-> (b -> Finite (Cardinality b)) -> b -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Finite (Cardinality b)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite)
    ((Finite (Cardinality b) -> b)
-> Maybe (Finite (Cardinality b)) -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite (Cardinality b) -> b
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Maybe (Finite (Cardinality b)) -> Maybe b)
-> (a -> Maybe (Finite (Cardinality b))) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> Maybe (Finite (Cardinality b))
forall (n :: Nat) (m :: Nat).
(KnownNat n, n <= m) =>
Finite m -> Maybe (Finite n)
strengthenN (Finite (Cardinality a) -> Maybe (Finite (Cardinality b)))
-> (a -> Finite (Cardinality a))
-> a
-> Maybe (Finite (Cardinality b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite)