ymdryo

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

newtype Heftia h a = Heftia {unHeftia :: FreerTreeT (h (Heftia h)) Identity a}
    deriving (Functor, Applicative, Monad)

to :: HFunctor h => Heftia h a -> HeftiaTree h a
to (Heftia (FreerTreeT (FreeT (Identity f)))) =
    HeftiaTreeT . HeftyT . Identity $ case f of

ymdryo

{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

module Control.HyperFree where

import Control.Applicative (Alternative)
import Control.Monad (MonadPlus)

ymdryo

{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

module Control.HyperFree where

import Control.Applicative (Alternative)
import Control.Monad (MonadPlus)

ymdryo

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

newtype
    HyperFree
        (f :: InsClass -> Type -> Type)
        (e :: ASigClass)
        (a :: Type) = HyperFree
    {unHyperFree :: (f :# GetSigClass e) a}

ymdryo

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

infixr 5 #+#, #+, +#, :+:

newtype
    (:+:)
        (e1 :: SigClass)
        (e2 :: SigClass)

ymdryo

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

sumH :: (e1 h e a -> r) -> (e2 h e a -> r) -> (e1 :+: e2) h e a -> r
sumH f g = caseSum f g . unSumH
{-# INLINE sumH #-}

swapSumH :: (e1 :+: e2) h e ~> (e2 :+: e1) h e
swapSumH = SumH . sumH R1 L1

ymdryo

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

class HFunctorT (e :: SigClass) where
    type HFTDict e :: ((Type -> Type) -> Type -> Type) -> Type
    type HFTDict _ = (:~:) IdentityT

    hfmapT :: (forall t. HFTDict e t -> t f ~> t g) -> e f ~> e g

ymdryo

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- This Source Code Form is subject to the terms of the Mozilla Public

ymdryo

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

module Control.Hefty where

import Control.Applicative (Alternative)

ymdryo

括弧が見づらいので()に加えて[],{}も括弧の代わりに使います
つまり[]はいわゆるHaskellのリストの型ではないので注意してください

まず前提として
Hefty h a = Return a | Op [h (Hefty h) (Hefty h a)]
Coyoneda f a = ∀b. (b -> a,  f b)
です
(cf. https://twitter.com/ymdfield/status/1743235218847465546)

ここでCoyonedaの高階版を定義します