{# LANGUAGE Trustworthy #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{
 Copyright (C) 2020 Koz Ross

 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 .
}
 
 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@retrofreedom.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) viceversa.

 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)