{-# 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 (fromFinite . toFinite) (fromFinite . 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'
    (fromFinite . weakenN . toFinite)
    (fmap fromFinite . strengthenN . toFinite)