Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Created July 30, 2022 05:20
Show Gist options
  • Save Icelandjack/7be54bded90e58c88b498af5d988d64c to your computer and use it in GitHub Desktop.
Save Icelandjack/7be54bded90e58c88b498af5d988d64c to your computer and use it in GitHub Desktop.
Implement product of datatypes in generics-sop: liftA2 (++) of codes
-- This witnesses multiplying two polynomials
--
-- Code (Maybe a) = [[], [a]]
-- Code (Maybe b) = [[], [b]]
--
-- Then the product of (Maybe a, Maybe b) is isomorphic to the
-- multiplication of their codes
--
-- Code (MegaMaybe a b) = [[], [a], [b], [a,b]]
--
-- With unit
--
-- Code () = [[]]
--
-- serving as identity
--
-- >> () × LT :: Ordering
-- LT
-- >> () × EQ :: Ordering
-- EQ
-- >> () × GT :: Ordering
-- GT
-- >> LT × () :: Ordering
-- LT
-- >> EQ × () :: Ordering
-- EQ
-- >> GT × () :: Ordering
-- GT
--
-- The operation of multiplication is equivalent to
--
-- liftA2 @[] (++)
--
-- where
--
-- liftA2 (++) [] _ = []
-- liftA2 (++) (a:as) bs = fmap (as ++) bs ++ liftA2 (++) as bs
--
-- And thus this gist defines a code that maps
--
-- SOP I ass -> SOP I bss -> SOP I (liftA2 (++) ass bss)
--
-- except implemented with type families.
--
-- >> (1, 2, 3) × () :: (Int, Int, Int)
-- (1,2,3)
-- >> (1, 2, 3) × Solo 4 :: (Int, Int, Int, Int)
-- (1,2,3,4)
-- >> (1, 2, 3) × (4, 5) :: (Int, Int, Int, Int, Int)
-- (1,2,3,4,5)
-- >> (1, 2, 3) × (4, 5, 6) :: (Int, Int, Int, Int, Int, Int)
-- (1,2,3,4,5,6)
-- >> (1, 2, 3) × (4, 5, 6, 7) :: (Int, Int, Int, Int, Int, Int, Int)
-- (1,2,3,4,5,6,7)
{-# Language AllowAmbiguousTypes #-}
{-# Language BlockArguments #-}
{-# Language DataKinds #-}
{-# Language DeriveAnyClass #-}
{-# Language DeriveGeneric #-}
{-# Language DerivingStrategies #-}
{-# Language FlexibleContexts #-}
{-# Language GADTs #-}
{-# Language ImportQualifiedPost #-}
{-# Language InstanceSigs #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}
import Data.Kind
import Generics.SOP
import Generics.SOP qualified as SOP
import Unsafe.Coerce
import GHC.Generics qualified as GHC
-- >> Nothing × Nothing :: MegaMaybe _ _
-- None
-- >> Nothing × Just 2 :: MegaMaybe _ _
-- Some1 2
-- >> Just 1 × Nothing :: MegaMaybe _ _
-- Some2 1
-- >> Just 1 × Just 2 :: MegaMaybe _ _
-- Some12 1 2
type MegaMaybe :: Type -> Type -> Type
data MegaMaybe a b = None | Some1 a | Some2 b | Some12 a b
deriving
stock (Show, GHC.Generic)
deriving
anyclass SOP.Generic
-- >> False × False :: MegaBool
-- FF
-- >> False × True :: MegaBool
-- FT
-- >> True × False :: MegaBool
-- TF
-- >> True × True :: MegaBool
-- TT
type MegaBool :: Type
data MegaBool = FF | FT | TF | TT
deriving
stock (Show, GHC.Generic)
deriving
anyclass SOP.Generic
(×) :: (LiftAppendContraint (Code a1) (Code a2), LiftAppendC (Code a1), Generic a3, Generic a1, Generic a2, Code a3 ~ LiftAppend (Code a1) (Code a2)) => a1 -> a2 -> a3
as × bs =
to do
SOP do
liftAppendC
do unSOP (from as)
do unSOP (from bs)
-- liftA2 (++) (as:ass) bss
-- = map (as ++) bss ++ liftA2 (++) ass bss
type
LiftAppend :: [[k]] -> [[k]] -> [[k]]
type family
LiftAppend ass bss where
LiftAppend '[] _ = '[]
LiftAppend (as:ass) bss = MapAppend as bss ++ LiftAppend ass bss
type LiftAppendC :: [[k]] -> Constraint
class LiftAppendC (ass :: [[k]]) where
type LiftAppendContraint ass (bss :: [[k]]) :: Constraint
liftAppendC :: LiftAppendContraint ass bss => NS (NP f) ass -> NS (NP f) bss -> NS (NP f) (LiftAppend ass bss)
instance LiftAppendC '[] where
type LiftAppendContraint '[] bss = ()
liftAppendC :: NS (NP f) '[] -> NS (NP f) bss -> NS (NP f) '[]
liftAppendC = const
instance LiftAppendC ass => LiftAppendC (as:ass) where
type LiftAppendContraint (as:ass) bss = (MapAppendC bss, MapAppendConstraint as bss, LiftAppendContraint ass bss, LengthC (MapAppend as bss))
liftAppendC :: forall f bss. MapAppendC bss => MapAppendConstraint as bss => LiftAppendContraint ass bss => LengthC (MapAppend as bss) => NS (NP f) (as:ass) -> NS (NP f) bss -> NS (NP f) (MapAppend as bss ++ LiftAppend ass bss)
liftAppendC (Z as) bss = shiftNS' @_ @_ @(LiftAppend ass bss) x where
x :: NS (NP f) (MapAppend as bss)
x = mapAppendC as bss
liftAppendC (S ass) bss = shiftNS len (liftAppendC ass bss) where
len :: Length (MapAppend as bss)
len = lengthC
type LengthC :: [k] -> Constraint
class LengthC as where
lengthC :: Length as
instance LengthC '[] where
lengthC :: Length '[]
lengthC = LZ
instance LengthC as => LengthC (a:as) where
lengthC :: Length (a:as)
lengthC = LS lengthC
type Length :: [k] -> Type
data Length as where
LZ :: Length '[]
LS :: Length as -> Length (a:as)
shiftNS' :: NS f as -> NS f (as ++ suffix)
shiftNS' = unsafeCoerce
shiftNS :: forall prefix f as. Length prefix -> NS f as -> NS f (prefix ++ as)
shiftNS prefix = go LZ where
go :: forall locals. Length locals -> NS f (locals ++ as) -> NS f (locals ++ prefix ++ as)
go LZ ns = weakenNS prefix ns
go (LS len) (Z local) = Z local
go (LS len) (S as) = S (go len as)
weakenNS :: Length prefix -> NS f xs -> NS f (prefix ++ xs)
weakenNS LZ sum = sum
weakenNS (LS len) sum = S (weakenNS len sum)
-- map (as ++) bss
type
MapAppend :: [k] -> [[k]] -> [[k]]
type family
MapAppend as bss where
MapAppend _ '[] = '[]
MapAppend as (bs:bss) = (as ++ bs) : MapAppend as bss
type MapAppendC :: [[k]] -> Constraint
class MapAppendC (bss :: [[k]]) where
type MapAppendConstraint (as :: [k]) (bss :: [[k]]) :: Constraint
mapAppendC
:: MapAppendConstraint as bss
=> NP f as
-> NS (NP f) bss
-> NS (NP f) (MapAppend as bss)
instance MapAppendC '[] where
type MapAppendConstraint as '[] = ()
mapAppendC :: NP f as -> NS (NP f) '[] -> NS (NP f) '[]
mapAppendC = const id
instance MapAppendC bss => MapAppendC (bs:bss) where
type MapAppendConstraint as (bs:bss) = (AppendProdC as, MapAppendConstraint as bss)
mapAppendC
:: forall as f. ()
=> AppendProdC as
=> MapAppendConstraint as bss
=> NP f as
-> NS (NP f) (bs:bss)
-> NS (NP f) ((as ++ bs) : MapAppend as bss)
mapAppendC as (Z bs) = Z cs where
cs :: NP f (as ++ bs)
cs = appendProdC as bs
mapAppendC as (S bs) = S cs where
cs :: NS (NP f) (MapAppend as bss)
cs = mapAppendC @_ @bss @as @f as bs
-- (++)
infixr 5 ++
type family
as ++ bs where
'[] ++ bs = bs
(a:as) ++ bs = a:(as ++ bs)
type AppendProdC :: [k] -> Constraint
class AppendProdC as where
appendProdC :: NP f as -> NP f bs -> NP f (as ++ bs)
instance AppendProdC '[] where
appendProdC :: NP f '[] -> NP f bs -> NP f bs
appendProdC = const id
instance AppendProdC as => AppendProdC (a:as) where
appendProdC :: NP f (a:as) -> NP f bs -> NP f (a:as ++ bs)
appendProdC (a :* as) bs = a :* appendProdC as bs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment