{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}

module Data.Polynomial.Functor.Deriving(
  ViaPolynomial(..),

  Zippy(..),
  Aligney(..)
) where

import Data.Kind (Type)

import Data.Singletons
import Data.Polynomial
import Control.Monad ((<=<))

import Data.Coerce

import Data.Polynomial.Functor

-- | Generic Deriving
newtype ViaPolynomial (e :: Poly -> Type -> Type) (f :: Type -> Type) a = ViaPolynomial { forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a.
ViaPolynomial e f a -> f a
unwrapViaPolynomial :: f a }
    deriving (forall a b.
 (a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b)
-> (forall a b. a -> ViaPolynomial e f b -> ViaPolynomial e f a)
-> Functor (ViaPolynomial e f)
forall a b. a -> ViaPolynomial e f b -> ViaPolynomial e f a
forall a b. (a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a b.
Functor f =>
a -> ViaPolynomial e f b -> ViaPolynomial e f a
forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a b.
Functor f =>
(a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b
$cfmap :: forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a b.
Functor f =>
(a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b
fmap :: forall a b. (a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b
$c<$ :: forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a b.
Functor f =>
a -> ViaPolynomial e f b -> ViaPolynomial e f a
<$ :: forall a b. a -> ViaPolynomial e f b -> ViaPolynomial e f a
Functor

instance PolynomialFunctor f => PolynomialFunctor (ViaPolynomial e f) where
    type PolyRep (ViaPolynomial _ f) = PolyRep f
    sPolyRep :: Sing (PolyRep (ViaPolynomial e f))
sPolyRep = forall (f :: Type -> Type). PolynomialFunctor f => Sing (PolyRep f)
sPolyRep @f
    toPoly :: forall x. ViaPolynomial e f x -> Ev (PolyRep (ViaPolynomial e f)) x
toPoly = f x -> Ev (PolyRep f) x
forall x. f x -> Ev (PolyRep f) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly (f x -> Ev (PolyRep f) x)
-> (ViaPolynomial e f x -> f x)
-> ViaPolynomial e f x
-> Ev (PolyRep f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ViaPolynomial e f x -> f x
forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a.
ViaPolynomial e f a -> f a
unwrapViaPolynomial
    fromPoly :: forall x. Ev (PolyRep (ViaPolynomial e f)) x -> ViaPolynomial e f x
fromPoly = f x -> ViaPolynomial e f x
forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a.
f a -> ViaPolynomial e f a
ViaPolynomial (f x -> ViaPolynomial e f x)
-> (Ev (PolyRep f) x -> f x)
-> Ev (PolyRep f) x
-> ViaPolynomial e f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ev (PolyRep f) x -> f x
forall x. Ev (PolyRep f) x -> f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly

instance (PolynomialFunctor f, p ~ PolyRep f, Coercible e Ev, Applicative (e p)) => Applicative (ViaPolynomial e f) where
    pure :: forall a. a -> ViaPolynomial e f a
    pure :: forall a. a -> ViaPolynomial e f a
pure = Ev p a -> ViaPolynomial e f a
Ev (PolyRep (ViaPolynomial e f)) a -> ViaPolynomial e f a
forall x. Ev (PolyRep (ViaPolynomial e f)) x -> ViaPolynomial e f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly (Ev p a -> ViaPolynomial e f a)
-> (a -> Ev p a) -> a -> ViaPolynomial e f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(e p a) @(Ev p a) (e p a -> Ev p a) -> (a -> e p a) -> a -> Ev p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> e p a
forall a. a -> e p a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure

    (<*>) :: forall a b. ViaPolynomial e f (a -> b) -> ViaPolynomial e f a -> ViaPolynomial e f b
    ViaPolynomial e f (a -> b)
fx <*> :: forall a b.
ViaPolynomial e f (a -> b)
-> ViaPolynomial e f a -> ViaPolynomial e f b
<*> ViaPolynomial e f a
fy = Ev (PolyRep (ViaPolynomial e f)) b -> ViaPolynomial e f b
forall x. Ev (PolyRep (ViaPolynomial e f)) x -> ViaPolynomial e f x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly (Ev (PolyRep (ViaPolynomial e f)) b -> ViaPolynomial e f b)
-> Ev (PolyRep (ViaPolynomial e f)) b -> ViaPolynomial e f b
forall a b. (a -> b) -> a -> b
$ e p b -> Ev p b
forall c. e p c -> Ev p c
coerceBwd (e p b -> Ev p b) -> e p b -> Ev p b
forall a b. (a -> b) -> a -> b
$ Ev p (a -> b) -> e p (a -> b)
forall c. Ev p c -> e p c
coerceFwd (ViaPolynomial e f (a -> b)
-> Ev (PolyRep (ViaPolynomial e f)) (a -> b)
forall x. ViaPolynomial e f x -> Ev (PolyRep (ViaPolynomial e f)) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly ViaPolynomial e f (a -> b)
fx) e p (a -> b) -> e p a -> e p b
forall a b. e p (a -> b) -> e p a -> e p b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Ev p a -> e p a
forall c. Ev p c -> e p c
coerceFwd (ViaPolynomial e f a -> Ev (PolyRep (ViaPolynomial e f)) a
forall x. ViaPolynomial e f x -> Ev (PolyRep (ViaPolynomial e f)) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly ViaPolynomial e f a
fy)
      where
        coerceFwd :: forall c. Ev p c -> e p c
        coerceFwd :: forall c. Ev p c -> e p c
coerceFwd = Ev p c -> e p c
forall a b. Coercible a b => a -> b
coerce
        coerceBwd :: forall c. e p c -> Ev p c
        coerceBwd :: forall c. e p c -> Ev p c
coerceBwd = e p c -> Ev p c
forall a b. Coercible a b => a -> b
coerce

instance (PolynomialFunctor f, p ~ PolyRep f, Coercible e Ev, Monad (e p)) => Monad (ViaPolynomial e f) where
    (>>=) :: forall a b. ViaPolynomial e f a -> (a -> ViaPolynomial e f b) -> ViaPolynomial e f b
    ViaPolynomial e f a
fx >>= :: forall a b.
ViaPolynomial e f a
-> (a -> ViaPolynomial e f b) -> ViaPolynomial e f b
>>= a -> ViaPolynomial e f b
k = f b -> ViaPolynomial e f b
forall (e :: Poly -> Type -> Type) (f :: Type -> Type) a.
f a -> ViaPolynomial e f a
ViaPolynomial (f b -> ViaPolynomial e f b) -> f b -> ViaPolynomial e f b
forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) x.
PolynomialFunctor f =>
Ev (PolyRep f) x -> f x
fromPoly @f (Ev (PolyRep f) b -> f b) -> Ev (PolyRep f) b -> f b
forall a b. (a -> b) -> a -> b
$ e p b -> Ev p b
forall c. e p c -> Ev p c
coerceBwd (e p b -> Ev p b) -> e p b -> Ev p b
forall a b. (a -> b) -> a -> b
$ Ev p a -> e p a
forall c. Ev p c -> e p c
coerceFwd (ViaPolynomial e f a -> Ev (PolyRep (ViaPolynomial e f)) a
forall x. ViaPolynomial e f x -> Ev (PolyRep (ViaPolynomial e f)) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly ViaPolynomial e f a
fx) e p a -> (a -> e p b) -> e p b
forall a b. e p a -> (a -> e p b) -> e p b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ev p b -> e p b
forall c. Ev p c -> e p c
coerceFwd (Ev p b -> e p b) -> (a -> Ev p b) -> a -> e p b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ViaPolynomial e f b -> Ev p b
ViaPolynomial e f b -> Ev (PolyRep (ViaPolynomial e f)) b
forall x. ViaPolynomial e f x -> Ev (PolyRep (ViaPolynomial e f)) x
forall (f :: Type -> Type) x.
PolynomialFunctor f =>
f x -> Ev (PolyRep f) x
toPoly (ViaPolynomial e f b -> Ev p b)
-> (a -> ViaPolynomial e f b) -> a -> Ev p b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ViaPolynomial e f b
k
      where
        coerceFwd :: forall c. Ev p c -> e p c
        coerceFwd :: forall c. Ev p c -> e p c
coerceFwd = Ev p c -> e p c
forall a b. Coercible a b => a -> b
coerce
        coerceBwd :: forall c. e p c -> Ev p c
        coerceBwd :: forall c. e p c -> Ev p c
coerceBwd = e p c -> Ev p c
forall a b. Coercible a b => a -> b
coerce




-- | Any polynomial functor @'Ev' p@ can have a "zippy" applicative instance.
--
-- == Example
-- 
-- >>> type P = 'S ('T ('S ('T 'U))) -- P(x) = 1 + x + x^2
-- >>> pure 0 :: Zippy P Int
-- Zippy {runZippy = Go (0 ::: Go (0 ::: End))}
-- >>> fx = Zippy $ Go ("A" ::: Go ("a" ::: End)) :: Zippy P String
-- >>> fy = Zippy $ Go ("B" ::: Stop) :: Zippy P String
-- >>> fz = Zippy $ Stop :: Zippy P String
-- >>> (++) <$> fx <*> fy
-- Zippy {runZippy = Go ("AB" ::: Stop)}
-- >>> (++) <$> fx <*> fz
-- Zippy {runZippy = Stop}
-- >>> (++) <$> fy <*> fz
-- Zippy {runZippy = Stop}
newtype Zippy p x = Zippy { forall (p :: Poly) x. Zippy p x -> Ev p x
runZippy :: Ev p x }
    deriving (Int -> Zippy p x -> ShowS
[Zippy p x] -> ShowS
Zippy p x -> String
(Int -> Zippy p x -> ShowS)
-> (Zippy p x -> String)
-> ([Zippy p x] -> ShowS)
-> Show (Zippy p x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (p :: Poly) x. Show x => Int -> Zippy p x -> ShowS
forall (p :: Poly) x. Show x => [Zippy p x] -> ShowS
forall (p :: Poly) x. Show x => Zippy p x -> String
$cshowsPrec :: forall (p :: Poly) x. Show x => Int -> Zippy p x -> ShowS
showsPrec :: Int -> Zippy p x -> ShowS
$cshow :: forall (p :: Poly) x. Show x => Zippy p x -> String
show :: Zippy p x -> String
$cshowList :: forall (p :: Poly) x. Show x => [Zippy p x] -> ShowS
showList :: [Zippy p x] -> ShowS
Show, Zippy p x -> Zippy p x -> Bool
(Zippy p x -> Zippy p x -> Bool)
-> (Zippy p x -> Zippy p x -> Bool) -> Eq (Zippy p x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (p :: Poly) x. Eq x => Zippy p x -> Zippy p x -> Bool
$c== :: forall (p :: Poly) x. Eq x => Zippy p x -> Zippy p x -> Bool
== :: Zippy p x -> Zippy p x -> Bool
$c/= :: forall (p :: Poly) x. Eq x => Zippy p x -> Zippy p x -> Bool
/= :: Zippy p x -> Zippy p x -> Bool
Eq, Eq (Zippy p x)
Eq (Zippy p x) =>
(Zippy p x -> Zippy p x -> Ordering)
-> (Zippy p x -> Zippy p x -> Bool)
-> (Zippy p x -> Zippy p x -> Bool)
-> (Zippy p x -> Zippy p x -> Bool)
-> (Zippy p x -> Zippy p x -> Bool)
-> (Zippy p x -> Zippy p x -> Zippy p x)
-> (Zippy p x -> Zippy p x -> Zippy p x)
-> Ord (Zippy p x)
Zippy p x -> Zippy p x -> Bool
Zippy p x -> Zippy p x -> Ordering
Zippy p x -> Zippy p x -> Zippy p x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (p :: Poly) x. Ord x => Eq (Zippy p x)
forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Bool
forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Ordering
forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Zippy p x
$ccompare :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Ordering
compare :: Zippy p x -> Zippy p x -> Ordering
$c< :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Bool
< :: Zippy p x -> Zippy p x -> Bool
$c<= :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Bool
<= :: Zippy p x -> Zippy p x -> Bool
$c> :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Bool
> :: Zippy p x -> Zippy p x -> Bool
$c>= :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Bool
>= :: Zippy p x -> Zippy p x -> Bool
$cmax :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Zippy p x
max :: Zippy p x -> Zippy p x -> Zippy p x
$cmin :: forall (p :: Poly) x. Ord x => Zippy p x -> Zippy p x -> Zippy p x
min :: Zippy p x -> Zippy p x -> Zippy p x
Ord, (forall a b. (a -> b) -> Zippy p a -> Zippy p b)
-> (forall a b. a -> Zippy p b -> Zippy p a) -> Functor (Zippy p)
forall a b. a -> Zippy p b -> Zippy p a
forall a b. (a -> b) -> Zippy p a -> Zippy p b
forall (p :: Poly) a b. a -> Zippy p b -> Zippy p a
forall (p :: Poly) a b. (a -> b) -> Zippy p a -> Zippy p b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (p :: Poly) a b. (a -> b) -> Zippy p a -> Zippy p b
fmap :: forall a b. (a -> b) -> Zippy p a -> Zippy p b
$c<$ :: forall (p :: Poly) a b. a -> Zippy p b -> Zippy p a
<$ :: forall a b. a -> Zippy p b -> Zippy p a
Functor, (forall m. Monoid m => Zippy p m -> m)
-> (forall m a. Monoid m => (a -> m) -> Zippy p a -> m)
-> (forall m a. Monoid m => (a -> m) -> Zippy p a -> m)
-> (forall a b. (a -> b -> b) -> b -> Zippy p a -> b)
-> (forall a b. (a -> b -> b) -> b -> Zippy p a -> b)
-> (forall b a. (b -> a -> b) -> b -> Zippy p a -> b)
-> (forall b a. (b -> a -> b) -> b -> Zippy p a -> b)
-> (forall a. (a -> a -> a) -> Zippy p a -> a)
-> (forall a. (a -> a -> a) -> Zippy p a -> a)
-> (forall a. Zippy p a -> [a])
-> (forall a. Zippy p a -> Bool)
-> (forall a. Zippy p a -> Int)
-> (forall a. Eq a => a -> Zippy p a -> Bool)
-> (forall a. Ord a => Zippy p a -> a)
-> (forall a. Ord a => Zippy p a -> a)
-> (forall a. Num a => Zippy p a -> a)
-> (forall a. Num a => Zippy p a -> a)
-> Foldable (Zippy p)
forall a. Eq a => a -> Zippy p a -> Bool
forall a. Num a => Zippy p a -> a
forall a. Ord a => Zippy p a -> a
forall m. Monoid m => Zippy p m -> m
forall a. Zippy p a -> Bool
forall a. Zippy p a -> Int
forall a. Zippy p a -> [a]
forall a. (a -> a -> a) -> Zippy p a -> a
forall m a. Monoid m => (a -> m) -> Zippy p a -> m
forall b a. (b -> a -> b) -> b -> Zippy p a -> b
forall a b. (a -> b -> b) -> b -> Zippy p a -> b
forall (p :: Poly) a. Eq a => a -> Zippy p a -> Bool
forall (p :: Poly) a. Num a => Zippy p a -> a
forall (p :: Poly) a. Ord a => Zippy p a -> a
forall (p :: Poly) m. Monoid m => Zippy p m -> m
forall (p :: Poly) a. Zippy p a -> Bool
forall (p :: Poly) a. Zippy p a -> Int
forall (p :: Poly) a. Zippy p a -> [a]
forall (p :: Poly) a. (a -> a -> a) -> Zippy p a -> a
forall (p :: Poly) m a. Monoid m => (a -> m) -> Zippy p a -> m
forall (p :: Poly) b a. (b -> a -> b) -> b -> Zippy p a -> b
forall (p :: Poly) a b. (a -> b -> b) -> b -> Zippy p a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (p :: Poly) m. Monoid m => Zippy p m -> m
fold :: forall m. Monoid m => Zippy p m -> m
$cfoldMap :: forall (p :: Poly) m a. Monoid m => (a -> m) -> Zippy p a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Zippy p a -> m
$cfoldMap' :: forall (p :: Poly) m a. Monoid m => (a -> m) -> Zippy p a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Zippy p a -> m
$cfoldr :: forall (p :: Poly) a b. (a -> b -> b) -> b -> Zippy p a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Zippy p a -> b
$cfoldr' :: forall (p :: Poly) a b. (a -> b -> b) -> b -> Zippy p a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Zippy p a -> b
$cfoldl :: forall (p :: Poly) b a. (b -> a -> b) -> b -> Zippy p a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Zippy p a -> b
$cfoldl' :: forall (p :: Poly) b a. (b -> a -> b) -> b -> Zippy p a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Zippy p a -> b
$cfoldr1 :: forall (p :: Poly) a. (a -> a -> a) -> Zippy p a -> a
foldr1 :: forall a. (a -> a -> a) -> Zippy p a -> a
$cfoldl1 :: forall (p :: Poly) a. (a -> a -> a) -> Zippy p a -> a
foldl1 :: forall a. (a -> a -> a) -> Zippy p a -> a
$ctoList :: forall (p :: Poly) a. Zippy p a -> [a]
toList :: forall a. Zippy p a -> [a]
$cnull :: forall (p :: Poly) a. Zippy p a -> Bool
null :: forall a. Zippy p a -> Bool
$clength :: forall (p :: Poly) a. Zippy p a -> Int
length :: forall a. Zippy p a -> Int
$celem :: forall (p :: Poly) a. Eq a => a -> Zippy p a -> Bool
elem :: forall a. Eq a => a -> Zippy p a -> Bool
$cmaximum :: forall (p :: Poly) a. Ord a => Zippy p a -> a
maximum :: forall a. Ord a => Zippy p a -> a
$cminimum :: forall (p :: Poly) a. Ord a => Zippy p a -> a
minimum :: forall a. Ord a => Zippy p a -> a
$csum :: forall (p :: Poly) a. Num a => Zippy p a -> a
sum :: forall a. Num a => Zippy p a -> a
$cproduct :: forall (p :: Poly) a. Num a => Zippy p a -> a
product :: forall a. Num a => Zippy p a -> a
Foldable, Functor (Zippy p)
Foldable (Zippy p)
(Functor (Zippy p), Foldable (Zippy p)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Zippy p a -> f (Zippy p b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Zippy p (f a) -> f (Zippy p a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Zippy p a -> m (Zippy p b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Zippy p (m a) -> m (Zippy p a))
-> Traversable (Zippy p)
forall (p :: Poly). Functor (Zippy p)
forall (p :: Poly). Foldable (Zippy p)
forall (p :: Poly) (m :: Type -> Type) a.
Monad m =>
Zippy p (m a) -> m (Zippy p a)
forall (p :: Poly) (f :: Type -> Type) a.
Applicative f =>
Zippy p (f a) -> f (Zippy p a)
forall (p :: Poly) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Zippy p a -> m (Zippy p b)
forall (p :: Poly) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Zippy p a -> f (Zippy p b)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Zippy p (m a) -> m (Zippy p a)
forall (f :: Type -> Type) a.
Applicative f =>
Zippy p (f a) -> f (Zippy p a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Zippy p a -> m (Zippy p b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Zippy p a -> f (Zippy p b)
$ctraverse :: forall (p :: Poly) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Zippy p a -> f (Zippy p b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Zippy p a -> f (Zippy p b)
$csequenceA :: forall (p :: Poly) (f :: Type -> Type) a.
Applicative f =>
Zippy p (f a) -> f (Zippy p a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Zippy p (f a) -> f (Zippy p a)
$cmapM :: forall (p :: Poly) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Zippy p a -> m (Zippy p b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Zippy p a -> m (Zippy p b)
$csequence :: forall (p :: Poly) (m :: Type -> Type) a.
Monad m =>
Zippy p (m a) -> m (Zippy p a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Zippy p (m a) -> m (Zippy p a)
Traversable)

instance SingI p => Applicative (Zippy p) where
    pure :: forall a. a -> Zippy p a
pure = Ev p a -> Zippy p a
forall (p :: Poly) x. Ev p x -> Zippy p x
Zippy (Ev p a -> Zippy p a) -> (a -> Ev p a) -> a -> Zippy p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing p -> a -> Ev p a
forall (p :: Poly) x. Sing p -> x -> Ev p x
pureZippy Sing p
forall {k} (a :: k). SingI a => Sing a
sing

    Zippy Ev p (a -> b)
fx <*> :: forall a b. Zippy p (a -> b) -> Zippy p a -> Zippy p b
<*> Zippy Ev p a
fy = Ev p b -> Zippy p b
forall (p :: Poly) x. Ev p x -> Zippy p x
Zippy (Ev p b -> Zippy p b) -> Ev p b -> Zippy p b
forall a b. (a -> b) -> a -> b
$ Ev p (a -> b) -> Ev p a -> Ev p b
forall (p :: Poly) a b. Ev p (a -> b) -> Ev p a -> Ev p b
apZippy Ev p (a -> b)
fx Ev p a
fy

pureZippy :: Sing p -> x -> Ev p x
pureZippy :: forall (p :: Poly) x. Sing p -> x -> Ev p x
pureZippy Sing p
SPoly p
SingU = Ev p x -> x -> Ev p x
forall a b. a -> b -> a
const Ev p x
Ev 'U x
forall x. Ev 'U x
End
pureZippy (SingS SPoly p
sp') = Ev p x -> Ev p x
Ev p x -> Ev ('S p) x
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go (Ev p x -> Ev p x) -> (x -> Ev p x) -> x -> Ev p x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing p -> x -> Ev p x
forall (p :: Poly) x. Sing p -> x -> Ev p x
pureZippy Sing p
SPoly p
sp'
pureZippy (SingT SPoly p
sp') =
    let pure' :: x -> Ev p x
pure' = Sing p -> x -> Ev p x
forall (p :: Poly) x. Sing p -> x -> Ev p x
pureZippy Sing p
SPoly p
sp'
    in \x
x -> x
x x -> Ev p x -> Ev ('T p) x
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: x -> Ev p x
pure' x
x

apZippy :: Ev p (a -> b) -> Ev p a -> Ev p b
apZippy :: forall (p :: Poly) a b. Ev p (a -> b) -> Ev p a -> Ev p b
apZippy Ev p (a -> b)
End Ev p a
_ = Ev p b
Ev 'U b
forall x. Ev 'U x
End
apZippy Ev p (a -> b)
Stop Ev p a
_ = Ev p b
Ev ('S p1) b
forall (p1 :: Poly) x. Ev ('S p1) x
Stop
apZippy Ev p (a -> b)
_ Ev p a
Stop = Ev p b
Ev ('S p1) b
forall (p1 :: Poly) x. Ev ('S p1) x
Stop
apZippy (Go Ev p1 (a -> b)
fx') (Go Ev p1 a
fy') = Ev p1 b -> Ev ('S p1) b
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go (Ev p1 (a -> b) -> Ev p1 a -> Ev p1 b
forall (p :: Poly) a b. Ev p (a -> b) -> Ev p a -> Ev p b
apZippy Ev p1 (a -> b)
fx' Ev p1 a
Ev p1 a
fy')
apZippy (a -> b
x ::: Ev p1 (a -> b)
fx') (a
y ::: Ev p1 a
fy') = a -> b
x a
y b -> Ev p1 b -> Ev ('T p1) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p1 (a -> b) -> Ev p1 a -> Ev p1 b
forall (p :: Poly) a b. Ev p (a -> b) -> Ev p a -> Ev p b
apZippy Ev p1 (a -> b)
fx' Ev p1 a
Ev p1 a
fy'

-- | Any polynomial functor /with no constant term/, @'Ev' (T p)@, can have an \"aligney\" applicative and monad instance.
-- 
-- == Example
-- 
-- >>> type Q = 'T ('S ('T 'U)) -- Q(x) = x + x^2
-- >>> pure 0 :: Aligney Q Int
-- Aligney {runAligney = 0 ::: Stop}
-- >>> fx = Aligney $ "A" ::: Go ("a" ::: End) :: Aligney Q String
-- >>> fy = Aligney $ "B" ::: Go ("b" ::: End) :: Aligney Q String
-- >>> fz = Aligney $ "C" ::: Stop :: Aligney Q String
-- >>> (++) <$> fx <*> fy
-- Aligney {runAligney = "AB" ::: Go ("ab" ::: End)}
-- >>> (++) <$> fx <*> fz
-- Aligney {runAligney = "AC" ::: Go ("aC" ::: End)}
-- >>> (++) <$> fy <*> fz
-- Aligney {runAligney = "BC" ::: Go ("bC" ::: End)}
-- >>> fx >>= \x -> if x == "A" then fz else fy
-- Aligney {runAligney = "C" ::: Go ("b" ::: End)}
newtype Aligney p x = Aligney { forall (p :: Poly) x. Aligney p x -> Ev p x
runAligney :: Ev p x }
    deriving (Int -> Aligney p x -> ShowS
[Aligney p x] -> ShowS
Aligney p x -> String
(Int -> Aligney p x -> ShowS)
-> (Aligney p x -> String)
-> ([Aligney p x] -> ShowS)
-> Show (Aligney p x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (p :: Poly) x. Show x => Int -> Aligney p x -> ShowS
forall (p :: Poly) x. Show x => [Aligney p x] -> ShowS
forall (p :: Poly) x. Show x => Aligney p x -> String
$cshowsPrec :: forall (p :: Poly) x. Show x => Int -> Aligney p x -> ShowS
showsPrec :: Int -> Aligney p x -> ShowS
$cshow :: forall (p :: Poly) x. Show x => Aligney p x -> String
show :: Aligney p x -> String
$cshowList :: forall (p :: Poly) x. Show x => [Aligney p x] -> ShowS
showList :: [Aligney p x] -> ShowS
Show, Aligney p x -> Aligney p x -> Bool
(Aligney p x -> Aligney p x -> Bool)
-> (Aligney p x -> Aligney p x -> Bool) -> Eq (Aligney p x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (p :: Poly) x. Eq x => Aligney p x -> Aligney p x -> Bool
$c== :: forall (p :: Poly) x. Eq x => Aligney p x -> Aligney p x -> Bool
== :: Aligney p x -> Aligney p x -> Bool
$c/= :: forall (p :: Poly) x. Eq x => Aligney p x -> Aligney p x -> Bool
/= :: Aligney p x -> Aligney p x -> Bool
Eq, Eq (Aligney p x)
Eq (Aligney p x) =>
(Aligney p x -> Aligney p x -> Ordering)
-> (Aligney p x -> Aligney p x -> Bool)
-> (Aligney p x -> Aligney p x -> Bool)
-> (Aligney p x -> Aligney p x -> Bool)
-> (Aligney p x -> Aligney p x -> Bool)
-> (Aligney p x -> Aligney p x -> Aligney p x)
-> (Aligney p x -> Aligney p x -> Aligney p x)
-> Ord (Aligney p x)
Aligney p x -> Aligney p x -> Bool
Aligney p x -> Aligney p x -> Ordering
Aligney p x -> Aligney p x -> Aligney p x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (p :: Poly) x. Ord x => Eq (Aligney p x)
forall (p :: Poly) x. Ord x => Aligney p x -> Aligney p x -> Bool
forall (p :: Poly) x.
Ord x =>
Aligney p x -> Aligney p x -> Ordering
forall (p :: Poly) x.
Ord x =>
Aligney p x -> Aligney p x -> Aligney p x
$ccompare :: forall (p :: Poly) x.
Ord x =>
Aligney p x -> Aligney p x -> Ordering
compare :: Aligney p x -> Aligney p x -> Ordering
$c< :: forall (p :: Poly) x. Ord x => Aligney p x -> Aligney p x -> Bool
< :: Aligney p x -> Aligney p x -> Bool
$c<= :: forall (p :: Poly) x. Ord x => Aligney p x -> Aligney p x -> Bool
<= :: Aligney p x -> Aligney p x -> Bool
$c> :: forall (p :: Poly) x. Ord x => Aligney p x -> Aligney p x -> Bool
> :: Aligney p x -> Aligney p x -> Bool
$c>= :: forall (p :: Poly) x. Ord x => Aligney p x -> Aligney p x -> Bool
>= :: Aligney p x -> Aligney p x -> Bool
$cmax :: forall (p :: Poly) x.
Ord x =>
Aligney p x -> Aligney p x -> Aligney p x
max :: Aligney p x -> Aligney p x -> Aligney p x
$cmin :: forall (p :: Poly) x.
Ord x =>
Aligney p x -> Aligney p x -> Aligney p x
min :: Aligney p x -> Aligney p x -> Aligney p x
Ord, (forall a b. (a -> b) -> Aligney p a -> Aligney p b)
-> (forall a b. a -> Aligney p b -> Aligney p a)
-> Functor (Aligney p)
forall a b. a -> Aligney p b -> Aligney p a
forall a b. (a -> b) -> Aligney p a -> Aligney p b
forall (p :: Poly) a b. a -> Aligney p b -> Aligney p a
forall (p :: Poly) a b. (a -> b) -> Aligney p a -> Aligney p b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (p :: Poly) a b. (a -> b) -> Aligney p a -> Aligney p b
fmap :: forall a b. (a -> b) -> Aligney p a -> Aligney p b
$c<$ :: forall (p :: Poly) a b. a -> Aligney p b -> Aligney p a
<$ :: forall a b. a -> Aligney p b -> Aligney p a
Functor, (forall m. Monoid m => Aligney p m -> m)
-> (forall m a. Monoid m => (a -> m) -> Aligney p a -> m)
-> (forall m a. Monoid m => (a -> m) -> Aligney p a -> m)
-> (forall a b. (a -> b -> b) -> b -> Aligney p a -> b)
-> (forall a b. (a -> b -> b) -> b -> Aligney p a -> b)
-> (forall b a. (b -> a -> b) -> b -> Aligney p a -> b)
-> (forall b a. (b -> a -> b) -> b -> Aligney p a -> b)
-> (forall a. (a -> a -> a) -> Aligney p a -> a)
-> (forall a. (a -> a -> a) -> Aligney p a -> a)
-> (forall a. Aligney p a -> [a])
-> (forall a. Aligney p a -> Bool)
-> (forall a. Aligney p a -> Int)
-> (forall a. Eq a => a -> Aligney p a -> Bool)
-> (forall a. Ord a => Aligney p a -> a)
-> (forall a. Ord a => Aligney p a -> a)
-> (forall a. Num a => Aligney p a -> a)
-> (forall a. Num a => Aligney p a -> a)
-> Foldable (Aligney p)
forall a. Eq a => a -> Aligney p a -> Bool
forall a. Num a => Aligney p a -> a
forall a. Ord a => Aligney p a -> a
forall m. Monoid m => Aligney p m -> m
forall a. Aligney p a -> Bool
forall a. Aligney p a -> Int
forall a. Aligney p a -> [a]
forall a. (a -> a -> a) -> Aligney p a -> a
forall m a. Monoid m => (a -> m) -> Aligney p a -> m
forall b a. (b -> a -> b) -> b -> Aligney p a -> b
forall a b. (a -> b -> b) -> b -> Aligney p a -> b
forall (p :: Poly) a. Eq a => a -> Aligney p a -> Bool
forall (p :: Poly) a. Num a => Aligney p a -> a
forall (p :: Poly) a. Ord a => Aligney p a -> a
forall (p :: Poly) m. Monoid m => Aligney p m -> m
forall (p :: Poly) a. Aligney p a -> Bool
forall (p :: Poly) a. Aligney p a -> Int
forall (p :: Poly) a. Aligney p a -> [a]
forall (p :: Poly) a. (a -> a -> a) -> Aligney p a -> a
forall (p :: Poly) m a. Monoid m => (a -> m) -> Aligney p a -> m
forall (p :: Poly) b a. (b -> a -> b) -> b -> Aligney p a -> b
forall (p :: Poly) a b. (a -> b -> b) -> b -> Aligney p a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (p :: Poly) m. Monoid m => Aligney p m -> m
fold :: forall m. Monoid m => Aligney p m -> m
$cfoldMap :: forall (p :: Poly) m a. Monoid m => (a -> m) -> Aligney p a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Aligney p a -> m
$cfoldMap' :: forall (p :: Poly) m a. Monoid m => (a -> m) -> Aligney p a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Aligney p a -> m
$cfoldr :: forall (p :: Poly) a b. (a -> b -> b) -> b -> Aligney p a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Aligney p a -> b
$cfoldr' :: forall (p :: Poly) a b. (a -> b -> b) -> b -> Aligney p a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Aligney p a -> b
$cfoldl :: forall (p :: Poly) b a. (b -> a -> b) -> b -> Aligney p a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Aligney p a -> b
$cfoldl' :: forall (p :: Poly) b a. (b -> a -> b) -> b -> Aligney p a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Aligney p a -> b
$cfoldr1 :: forall (p :: Poly) a. (a -> a -> a) -> Aligney p a -> a
foldr1 :: forall a. (a -> a -> a) -> Aligney p a -> a
$cfoldl1 :: forall (p :: Poly) a. (a -> a -> a) -> Aligney p a -> a
foldl1 :: forall a. (a -> a -> a) -> Aligney p a -> a
$ctoList :: forall (p :: Poly) a. Aligney p a -> [a]
toList :: forall a. Aligney p a -> [a]
$cnull :: forall (p :: Poly) a. Aligney p a -> Bool
null :: forall a. Aligney p a -> Bool
$clength :: forall (p :: Poly) a. Aligney p a -> Int
length :: forall a. Aligney p a -> Int
$celem :: forall (p :: Poly) a. Eq a => a -> Aligney p a -> Bool
elem :: forall a. Eq a => a -> Aligney p a -> Bool
$cmaximum :: forall (p :: Poly) a. Ord a => Aligney p a -> a
maximum :: forall a. Ord a => Aligney p a -> a
$cminimum :: forall (p :: Poly) a. Ord a => Aligney p a -> a
minimum :: forall a. Ord a => Aligney p a -> a
$csum :: forall (p :: Poly) a. Num a => Aligney p a -> a
sum :: forall a. Num a => Aligney p a -> a
$cproduct :: forall (p :: Poly) a. Num a => Aligney p a -> a
product :: forall a. Num a => Aligney p a -> a
Foldable, Functor (Aligney p)
Foldable (Aligney p)
(Functor (Aligney p), Foldable (Aligney p)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Aligney p a -> f (Aligney p b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Aligney p (f a) -> f (Aligney p a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Aligney p a -> m (Aligney p b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Aligney p (m a) -> m (Aligney p a))
-> Traversable (Aligney p)
forall (p :: Poly). Functor (Aligney p)
forall (p :: Poly). Foldable (Aligney p)
forall (p :: Poly) (m :: Type -> Type) a.
Monad m =>
Aligney p (m a) -> m (Aligney p a)
forall (p :: Poly) (f :: Type -> Type) a.
Applicative f =>
Aligney p (f a) -> f (Aligney p a)
forall (p :: Poly) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Aligney p a -> m (Aligney p b)
forall (p :: Poly) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Aligney p a -> f (Aligney p b)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Aligney p (m a) -> m (Aligney p a)
forall (f :: Type -> Type) a.
Applicative f =>
Aligney p (f a) -> f (Aligney p a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Aligney p a -> m (Aligney p b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Aligney p a -> f (Aligney p b)
$ctraverse :: forall (p :: Poly) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Aligney p a -> f (Aligney p b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Aligney p a -> f (Aligney p b)
$csequenceA :: forall (p :: Poly) (f :: Type -> Type) a.
Applicative f =>
Aligney p (f a) -> f (Aligney p a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Aligney p (f a) -> f (Aligney p a)
$cmapM :: forall (p :: Poly) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Aligney p a -> m (Aligney p b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Aligney p a -> m (Aligney p b)
$csequence :: forall (p :: Poly) (m :: Type -> Type) a.
Monad m =>
Aligney p (m a) -> m (Aligney p a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Aligney p (m a) -> m (Aligney p a)
Traversable)

instance SingI p => Applicative (Aligney (T p)) where
    pure :: forall a. a -> Aligney ('T p) a
pure = Ev ('T p) a -> Aligney ('T p) a
forall (p :: Poly) x. Ev p x -> Aligney p x
Aligney (Ev ('T p) a -> Aligney ('T p) a)
-> (a -> Ev ('T p) a) -> a -> Aligney ('T p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing ('T p) -> a -> Ev ('T p) a
forall (p :: Poly) x. Sing p -> x -> Ev p x
pureAligney Sing ('T p)
forall {k} (a :: k). SingI a => Sing a
sing
    Aligney Ev ('T p) (a -> b)
fx <*> :: forall a b.
Aligney ('T p) (a -> b) -> Aligney ('T p) a -> Aligney ('T p) b
<*> Aligney Ev ('T p) a
fy = Ev ('T p) b -> Aligney ('T p) b
forall (p :: Poly) x. Ev p x -> Aligney p x
Aligney (Ev ('T p) (a -> b) -> Ev ('T p) a -> Ev ('T p) b
forall (p :: Poly) a b.
Ev ('T p) (a -> b) -> Ev ('T p) a -> Ev ('T p) b
apAligney Ev ('T p) (a -> b)
fx Ev ('T p) a
fy)

pureAligney :: Sing p -> x -> Ev p x
pureAligney :: forall (p :: Poly) x. Sing p -> x -> Ev p x
pureAligney Sing p
SPoly p
SingU x
_ = Ev p x
Ev 'U x
forall x. Ev 'U x
End
pureAligney (SingS SPoly p
_) x
_ = Ev p x
Ev ('S p) x
forall (p1 :: Poly) x. Ev ('S p1) x
Stop
pureAligney (SingT SPoly p
sp') x
x = x
x x -> Ev p x -> Ev ('T p) x
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Sing p -> x -> Ev p x
forall (p :: Poly) x. Sing p -> x -> Ev p x
pureAligney Sing p
SPoly p
sp' x
x

apAligney :: Ev (T p) (a -> b) -> Ev (T p) a -> Ev (T p) b
apAligney :: forall (p :: Poly) a b.
Ev ('T p) (a -> b) -> Ev ('T p) a -> Ev ('T p) b
apAligney (a -> b
x ::: Ev p1 (a -> b)
fx') (a
y ::: Ev p1 a
fy') = a -> b
x a
y b -> Ev p b -> Ev ('T p) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: (a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
forall a b (p :: Poly).
(a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
apAlignAux a -> b
x a
y Ev p (a -> b)
Ev p1 (a -> b)
fx' Ev p a
Ev p1 a
fy'

apAlignAux :: (a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
apAlignAux :: forall a b (p :: Poly).
(a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
apAlignAux a -> b
x a
y Ev p (a -> b)
fx Ev p a
fy = case (Ev p (a -> b)
fx, Ev p a
fy) of
    (Ev p (a -> b)
End, Ev p a
End) -> Ev p b
Ev 'U b
forall x. Ev 'U x
End
    (Ev p (a -> b)
Stop, Ev p a
Stop) -> Ev p b
Ev ('S p1) b
forall (p1 :: Poly) x. Ev ('S p1) x
Stop
    (Ev p (a -> b)
Stop, Go Ev p1 a
fy') -> Ev p1 b -> Ev ('S p1) b
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go (a -> b
x (a -> b) -> Ev p1 a -> Ev p1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Ev p1 a
fy')
    (Go Ev p1 (a -> b)
fx', Ev p a
Stop) -> Ev p1 b -> Ev ('S p1) b
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go (((a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a
y) ((a -> b) -> b) -> Ev p1 (a -> b) -> Ev p1 b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Ev p1 (a -> b)
fx')
    (Go Ev p1 (a -> b)
fx', Go Ev p1 a
fy') -> Ev p1 b -> Ev ('S p1) b
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go ((a -> b) -> a -> Ev p1 (a -> b) -> Ev p1 a -> Ev p1 b
forall a b (p :: Poly).
(a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
apAlignAux a -> b
x a
y Ev p1 (a -> b)
fx' Ev p1 a
Ev p1 a
fy')
    (a -> b
x' ::: Ev p1 (a -> b)
fx', a
y' ::: Ev p1 a
fy') -> a -> b
x' a
y' b -> Ev p1 b -> Ev ('T p1) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: (a -> b) -> a -> Ev p1 (a -> b) -> Ev p1 a -> Ev p1 b
forall a b (p :: Poly).
(a -> b) -> a -> Ev p (a -> b) -> Ev p a -> Ev p b
apAlignAux a -> b
x' a
y' Ev p1 (a -> b)
fx' Ev p1 a
Ev p1 a
fy'

instance SingI p => Monad (Aligney (T p)) where
    Aligney Ev ('T p) a
fx >>= :: forall a b.
Aligney ('T p) a -> (a -> Aligney ('T p) b) -> Aligney ('T p) b
>>= a -> Aligney ('T p) b
k = Ev ('T p) b -> Aligney ('T p) b
forall (p :: Poly) x. Ev p x -> Aligney p x
Aligney (Ev ('T p) b -> Aligney ('T p) b)
-> Ev ('T p) b -> Aligney ('T p) b
forall a b. (a -> b) -> a -> b
$ Ev ('T p) a -> (a -> Ev ('T p) b) -> Ev ('T p) b
forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Ev ('T p) b) -> Ev ('T p) b
bindAligney Ev ('T p) a
fx (Aligney ('T p) b -> Ev ('T p) b
forall (p :: Poly) x. Aligney p x -> Ev p x
runAligney (Aligney ('T p) b -> Ev ('T p) b)
-> (a -> Aligney ('T p) b) -> a -> Ev ('T p) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Aligney ('T p) b
k)

headPoly :: Ev (T p) x -> x
headPoly :: forall (p :: Poly) x. Ev ('T p) x -> x
headPoly (x
x ::: Ev p1 x
_) = x
x
tailPoly :: Ev (T p) x -> Ev p x
tailPoly :: forall (p :: Poly) x. Ev ('T p) x -> Ev p x
tailPoly (x
_ ::: Ev p1 x
fx) = Ev p x
Ev p1 x
fx

bindAligney :: Ev ('T p) a -> (a -> Ev ('T p) b) -> Ev ('T p) b
bindAligney :: forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Ev ('T p) b) -> Ev ('T p) b
bindAligney Ev ('T p) a
fx a -> Ev ('T p) b
k = Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
bindAligney' Ev ('T p) a
fx (Ev ('T p) b -> Either b (Ev ('T p) b)
forall a b. b -> Either a b
Right (Ev ('T p) b -> Either b (Ev ('T p) b))
-> (a -> Ev ('T p) b) -> a -> Either b (Ev ('T p) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ev ('T p) b
k)

bindAligney' :: Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
bindAligney' :: forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
bindAligney' ((:::) a
x Ev p1 a
fx) a -> Either b (Ev ('T p) b)
k = case Ev p1 a
fx of
    Ev p1 a
End -> (b -> Ev ('T p) b)
-> (Ev ('T p) b -> Ev ('T p) b)
-> Either b (Ev ('T p) b)
-> Ev ('T p) b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> Ev p b -> Ev ('T p) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p b
Ev 'U b
forall x. Ev 'U x
End) Ev ('T p) b -> Ev ('T p) b
forall a. a -> a
id (Either b (Ev ('T p) b) -> Ev ('T p) b)
-> Either b (Ev ('T p) b) -> Ev ('T p) b
forall a b. (a -> b) -> a -> b
$ a -> Either b (Ev ('T p) b)
k a
x
    Ev p1 a
Stop -> (b -> Ev ('T p) b)
-> (Ev ('T p) b -> Ev ('T p) b)
-> Either b (Ev ('T p) b)
-> Ev ('T p) b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> Ev p b -> Ev ('T p) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p b
Ev ('S p1) b
forall (p1 :: Poly) x. Ev ('S p1) x
Stop) Ev ('T p) b -> Ev ('T p) b
forall a. a -> a
id (Either b (Ev ('T p) b) -> Ev ('T p) b)
-> Either b (Ev ('T p) b) -> Ev ('T p) b
forall a b. (a -> b) -> a -> b
$ a -> Either b (Ev ('T p) b)
k a
x
    Go Ev p1 a
fx' ->
        let b
z ::: Ev p1 b
Ev p1 b
fz' = Ev ('T p1) a -> (a -> Either b (Ev ('T p1) b)) -> Ev ('T p1) b
forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
bindAligney' (a
x a -> Ev p1 a -> Ev ('T p1) a
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p1 a
fx') (Ev ('T ('S p1)) b -> Either b (Ev ('T p1) b)
forall (p :: Poly) a. Ev ('T ('S p)) a -> Either a (Ev ('T p) a)
lowerPolyS (Ev ('T ('S p1)) b -> Either b (Ev ('T p1) b))
-> (a -> Either b (Ev ('T ('S p1)) b))
-> a
-> Either b (Ev ('T p1) b)
forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a -> Either b (Ev ('T p) b)
a -> Either b (Ev ('T ('S p1)) b)
k)
        in b
z b -> Ev p b -> Ev ('T p) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p1 b -> Ev ('S p1) b
forall (p1 :: Poly) x. Ev p1 x -> Ev ('S p1) x
Go Ev p1 b
fz'
    a
x' ::: Ev p1 a
fx' ->
        let z :: b
z = (b -> b) -> (Ev ('T p) b -> b) -> Either b (Ev ('T p) b) -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id Ev ('T p) b -> b
forall (p :: Poly) x. Ev ('T p) x -> x
headPoly (a -> Either b (Ev ('T p) b)
k a
x)
            fz :: Ev ('T p1) b
fz = Ev ('T p1) a -> (a -> Either b (Ev ('T p1) b)) -> Ev ('T p1) b
forall (p :: Poly) a b.
Ev ('T p) a -> (a -> Either b (Ev ('T p) b)) -> Ev ('T p) b
bindAligney' (a
x' a -> Ev p1 a -> Ev ('T p1) a
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p1 a
fx') ((Ev ('T ('T p1)) b -> Ev ('T p1) b)
-> Either b (Ev ('T ('T p1)) b) -> Either b (Ev ('T p1) b)
forall a b. (a -> b) -> Either b a -> Either b b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Ev ('T ('T p1)) b -> Ev ('T p1) b
forall (p :: Poly) x. Ev ('T p) x -> Ev p x
tailPoly (Either b (Ev ('T ('T p1)) b) -> Either b (Ev ('T p1) b))
-> (a -> Either b (Ev ('T ('T p1)) b))
-> a
-> Either b (Ev ('T p1) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b (Ev ('T p) b)
a -> Either b (Ev ('T ('T p1)) b)
k)
        in b
z b -> Ev p b -> Ev ('T p) b
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p b
Ev ('T p1) b
fz

lowerPolyS :: Ev ('T ('S p)) a -> Either a (Ev ('T p) a)
lowerPolyS :: forall (p :: Poly) a. Ev ('T ('S p)) a -> Either a (Ev ('T p) a)
lowerPolyS (a
x ::: Ev p1 a
Stop) = a -> Either a (Ev ('T p) a)
forall a b. a -> Either a b
Left a
x
lowerPolyS (a
x ::: Go Ev p1 a
fx) = Ev ('T p) a -> Either a (Ev ('T p) a)
forall a b. b -> Either a b
Right (a
x a -> Ev p a -> Ev ('T p) a
forall x (p1 :: Poly). x -> Ev p1 x -> Ev ('T p1) x
::: Ev p a
Ev p1 a
fx)