Squeeze.cabal

cabal-version: 2.4
name: Squeeze
version: 0.1.0.0
author: Ignat Insarov
maintainer: kindaro@gmail.com

library
  hs-source-dirs: .
  build-depends: base, distributive
  default-language: Haskell2010
  exposed-modules: Squeeze

Squeeze.hs

{-# LANGUAGE UnicodeSyntax  #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE BlockArguments #-}

module Squeeze where

import Data.Kind
import Data.Type.Equality
import GHC.TypeNats
import Data.Bifunctor
import Data.Tuple
import Data.Proxy
import Data.Distributive
import Data.Char

-- | Apply a constraint to a list of types.
type family ForAll (stuff :: [kind]) (constraint :: kind -> Constraint) :: Constraint where
  ForAll '[ ] constraint = ( )
  ForAll (atom: stuff) constraint = (constraint atom, ForAll stuff constraint)

-- | Peel the fruit until we get down to the seed.
type Strip :: Type -> Type -> [Type -> Type]
type family Strip seed fruit where
  Strip seed seed = '[ ]
  Strip seed (peel fruit) = peel: Strip seed fruit

-- | Given some peel, undo the peeling of a seed.
type Dress :: Type -> [Type -> Type] -> Type
type family Dress seed peel where
  Dress seed '[ ] = seed
  Dress seed (peel: peels) = peel (Dress seed peels)

-- | The common peels of two given fruits.
type family Peels apple pear where
  Peels (peel apple) (peel pear) = peel: Peels apple pear
  Peels _ _ = '[ ]

-- | The left projection of the type level tuple.
type family Π₁  tuple where
  Π₁ '(t₁, t₂) = t₁

-- | The right projection of the type level tuple.
type family Π₂ tuple where
  Π₂ '(t₁, t₂) = t₂

-- | What is left after peeling common peels off of two given fruits.
type Seeds :: Type -> Type -> (Type, Type)
type family Seeds apple pear where
  Seeds (peel apple) (peel pear) = Seeds apple pear
  Seeds apple pear = '(apple, pear)

type Not ∷ Bool → Bool
type family Not boolean where
  Not True = False
  Not False = True

type IsInductive seed fruit = Not (Strip seed fruit == '[ ])

-- | A fruit as a functor over its seed.
data Squeezed (boxes :: [Type -> Type]) contents where
  Identify :: contents -> Squeezed '[ ] contents
  Composify :: box (Squeezed boxes contents) -> Squeezed (box: boxes) contents

-- | So far as all the peels are functors, the squeezed fruit is a functor.
instance ForAll boxes Functor => Functor (Squeezed boxes) where
  fmap function (Identify contents) = Identify (function contents)
  fmap function (Composify box) = Composify (fmap (fmap function) box)

-- | We can elide `recursive` later but for now we need it for GHC to approve of
-- our functional dependencies.
class Squeezy' seed fruit (peels :: [Type -> Type]) (recursive :: Bool)
  | seed peels -> fruit, peels fruit -> seed, seed fruit recursive -> peels, seed fruit peels -> recursive where
  squeeze :: fruit -> Squeezed peels seed
  stretch :: Squeezed peels seed -> fruit

-- | We can squeeze a seed. It has no peels.
instance Squeezy' seed seed '[ ] False where
  squeeze = Identify
  stretch (Identify seed) = seed

-- | We can squeeze a fruit recursively, peel after peel.
instance (Functor peel, Squeezy' seed fruit peels recursive, recursive ~ IsInductive seed fruit)
  =>  Squeezy' seed (peel fruit) (peel: peels) True where
  squeeze = Composify . fmap squeeze
  stretch (Composify boxes) = fmap stretch boxes

-- | We can squeeze any fruit and stretch it back.
type Squeezy seed fruit peels = Squeezy' seed fruit peels (IsInductive seed fruit)

-- | The constraint that says that the same peels are applied to two different
-- seeds. `fmaps` requires this, so one way to think of it as the generalized
-- `Functor` constraint.
type Functors seed seed' peels =
  ( ForAll peels Functor
  , Squeezy seed (Dress seed peels) peels
  , Squeezy seed' (Dress seed' peels) peels )

-- | The ultimate `fmap`.
fmaps
  :: forall peels seed seed'. Functors seed seed' peels
  => (seed -> seed') -> Dress seed peels -> Dress seed' peels
fmaps function = stretch . fmap @(Squeezed peels) function . squeeze

-- | This is the right tensorial strength of a functor with respect to tupling.
deasil :: Functor functor => (functor left, right) -> functor (left, right)
deasil (functor, value) = fmap (, value) functor

-- | Generalized right tensorial strength.
deasils
  :: forall apple pear value.
  ( apple ~ Dress (Π₁ (Seeds apple pear)) (Peels apple pear)
  , pear ~ Dress (Π₂ (Seeds apple pear)) (Peels apple pear)
  , (Π₁ (Seeds apple pear), value) ~ Π₂ (Seeds apple pear)
  , Squeezy (Π₁ (Seeds apple pear)) apple (Peels apple pear)
  , Squeezy (Π₂ (Seeds apple pear)) pear (Peels apple pear)
  , ForAll (Peels apple pear) Functor )
  => (apple, value) -> pear
deasils (apple, value) = fmaps @(Peels apple pear) @(Π₁ (Seeds apple pear)) (, value) apple

instance Distributive (Squeezed '[ ]) where
  distribute = Identify . fmap (\ (Identify value) -> value)

instance (Distributive (Squeezed peels), Distributive peel, ForAll peels Functor) => Distributive (Squeezed (peel: peels)) where
  distribute = Composify . fmap distribute . distribute @peel . fmap (\ (Composify value) -> value)

distributify
  :: forall functor apple pear.
  ( apple ~ Dress (Π₁ (Seeds apple pear)) (Peels apple pear)
  , pear ~ Dress (Π₂ (Seeds apple pear)) (Peels apple pear)
  , functor (Π₁ (Seeds apple pear)) ~ Π₂ (Seeds apple pear)
  , Squeezy (Π₁ (Seeds apple pear)) apple (Peels apple pear)
  , Squeezy (Π₂ (Seeds apple pear)) pear (Peels apple pear)
  , ForAll (Peels apple pear) Distributive
  , Functor functor, Distributive (Squeezed (Peels apple pear)) )
  => functor apple -> pear
distributify = stretch . distribute . fmap (squeeze @_ @_ @(Peels apple pear))

example1 :: Maybe [String]
example1 = fmaps (show @Int) (Just [1, 2])

example2 :: Maybe String
example2 = fmaps (show @[Int]) (Just [1, 2])

example3 :: Maybe [(Bool, Char)]
example3 = deasils (Just [True, False], 'a')

example4 :: Int -> Char -> Maybe Bool
example4 = distributify (Just $ \ int char -> ord char == int)

type Arrow :: [★] → ★ → ★
type family Arrow arguments result where
  Arrow '[ ] result = result
  Arrow (argument: arguments) result = argument → Arrow arguments result

type Tuple ∷ [★] → ★
type family Tuple arguments = tuple | tuple → arguments where
  Tuple '[ ] = ( )
  Tuple (argument: arguments) = (argument, Tuple arguments)

type Curry ∷ ★ → ★ → [★] → Bool → Constraint
class Curry result arrow arguments inductive
  | result arguments -> arrow, arguments arrow -> result, result arrow inductive -> arguments, result arrow arguments -> inductive
  where
    rightwards ∷ (Tuple arguments → result) → arrow
    leftwards ∷ arrow → Tuple arguments → result

instance Curry result result '[ ] False
  where
    rightwards = ($ ( ))
    leftwards = const

instance {-# overlapping #-}
  (arrow ~ Arrow arguments result, Curry result arrow arguments (IsInductive result arrow)) ⇒
  Curry result (argument → arrow) (argument: arguments) True
  where
    rightwards function argument = rightwards (curry function argument)
    leftwards gunction (argument, arguments) = leftwards (gunction argument) arguments

example5 ∷ (Int, (Char, ( ))) → Bool
example5 = leftwards \ int char → ord char == int

example6 :: Int -> Char -> Bool
example6 = currify \ (int, (char, ( ))) -> ord char == int