Skip to content

Instantly share code, notes, and snippets.

@kindaro
Last active June 16, 2022 08:19
Show Gist options
  • Save kindaro/6056f753bcf356ced96b817fee72533c to your computer and use it in GitHub Desktop.
Save kindaro/6056f753bcf356ced96b817fee72533c to your computer and use it in GitHub Desktop.
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
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment