Skip to content

Instantly share code, notes, and snippets.

@sheaf

sheaf/Shape.hs

Last active September 13, 2022 10:48
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save sheaf/769a254bf4df9166bb73c158bd393df7 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save sheaf/769a254bf4df9166bb73c158bd393df7 to your computer and use it in GitHub Desktop.
Download ZIP
Shape and contents of a traversable value (cofree traversable)
Raw
Shape.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Shape
( Shape(Shape)
, disassemble, reassemble
) where
-- base
import Data.Kind
( Type, Constraint )
import Numeric.Natural
( Natural )
import Unsafe.Coerce
( unsafeCoerce )
-------------------------------------------------------------------------------
-- Graded bialgebras.
type GradedBialgebra :: ( Nat -> Type -> Type ) -> Constraint
class GradedBialgebra g where
degree :: g i a -> SNat i
unit :: g Z a
(<!>) :: g i a -> g j a -> g (i+j) a
(>!<) :: g (i+j) a -> SNat i -> ( g i a, g j a )
type Endo :: ( Nat -> Type -> Type ) -> Type -> Type -> Type -> Type
data Endo g a b c where
Endo :: g n a -> ( g n b -> c ) -> Endo g a b c
type Gen :: ( Nat -> Type -> Type ) -> Type
type GenT :: ( Type -> Type ) -> ( Nat -> Type -> Type ) -> Type
type Gen g = forall a b. a -> Endo g a b b
type GenT t g = forall a b. t a -> Endo g a b (t b)
instance Functor (Endo g a b) where
fmap f (Endo v g) = Endo v ( f . g )
instance GradedBialgebra g => Applicative (Endo g a b) where
pure c = Endo unit (const c)
(Endo v f) <*> (Endo w g) = Endo vw fg
where
vw = v <!> w
fg ( ( >!< degree v ) -> ( u1, u2 ) ) = f u1 $ g u2
-- 'V' is the free graded bialgebra on one generator (homogeneous, of degree 1).
instance GradedBialgebra V where
unit = Nil
(<!>) = mappendV
(>!<) = flip splitAtV
degree = lengthV
gen :: Gen V
gen a = Endo ( a :. Nil ) ( \ ( b :. _ ) -> b )
genT :: Traversable t => GenT t V
genT = traverse gen
-------------------------------------------------------------------------------
-- Co-free traversable.
-- Shape and contents of a traversable value.
type Shape :: ( Type -> Type ) -> Type -> Type
data Shape f a where
Shape :: f (Fin n) -> V n a -> Shape f a
deriving stock instance ( Show a, forall b. Show b => Show (f b) ) => Show (Shape f a)
deriving stock instance Functor (Shape f)
deriving stock instance Foldable (Shape f)
deriving stock instance Traversable (Shape f)
reassemble :: Functor f => Shape f a -> f a
reassemble (Shape i v) = fmap ( at v ) i
disassemble :: forall t a. Traversable t => t a -> Shape t a
disassemble ta = case genT ta of
Endo (v :: V n a) (f :: V n Nat -> t Nat) ->
Shape ( coerceNatFin f ( range n ) ) v
where n = lengthV v
------------------------------------------------------------------------------
------------------------------------------------------------------------------
---- End of interesting code, basic Nat / Fin / Vec library code follows. ----
------------------------------------------------------------------------------
------------------------------------------------------------------------------
---------------------------------
-- Peano natural numbers.
data Nat where
Z :: Nat
S :: Nat -> Nat
toNatural :: Nat -> Natural
toNatural Z = 0
toNatural (S n) = succ ( toNatural n )
instance Show Nat where
show i = show ( toNatural i )
type family (i :: Nat) + (j :: Nat) :: Nat where
Z + j = j
(S i) + j = S (i + j)
data SNat :: Nat -> Type where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
natVal :: SNat n -> Nat
natVal SZ = Z
natVal (SS n) = S ( natVal n )
instance Show (SNat n) where
show i = show ( toNatural (natVal i) )
class KnownNat (n :: Nat) where
natSing :: SNat n
instance KnownNat Z where
natSing = SZ
instance KnownNat n => KnownNat (S n) where
natSing = SS ( natSing @n )
data Fin (n :: Nat) where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
finToNat :: Fin n -> Nat
finToNat FZ = Z
finToNat (FS i) = S ( finToNat i )
instance Show (Fin n) where
show i = "Fin " ++ show ( finToNat i )
coerceNatFin :: ( f Nat -> g Nat ) -> ( f (Fin n) -> g (Fin n) )
coerceNatFin = unsafeCoerce
---------------------------------
-- Sized vectors.
infixr 3 :.
data V (n :: Nat) (a :: Type) where
Nil :: V Z a
(:.) :: a -> V n a -> V (S n) a
deriving stock instance Show a => Show (V n a)
deriving stock instance Functor (V n)
deriving stock instance Foldable (V n)
deriving stock instance Traversable (V n)
buildV :: forall n a. SNat n -> ( Fin n -> a ) -> V n a
buildV SZ _ = Nil
buildV (SS n) f = f FZ :. buildV n ( f . FS )
range :: SNat n -> V n (Fin n)
range n = buildV n id
type family KnownNatsUpTo (n :: Nat) :: Constraint where
KnownNatsUpTo Z = ()
KnownNatsUpTo (S n) = ( KnownNat n, KnownNatsUpTo n )
instance ( KnownNat n, KnownNatsUpTo n ) => Applicative (V n) where
pure = buildV (natSing @n) . const
_ <*> Nil = Nil
(f :. fs) <*> (a :. as) = f a :. fs <*> as
mappendV :: V i a -> V j a -> V (i+j) a
mappendV Nil v = v
mappendV (a :. as) v = a :. (as `mappendV` v)
splitAtV :: SNat i -> V (i+j) a -> (V i a, V j a)
splitAtV SZ v = ( Nil, v )
splitAtV (SS i) (a :. as) = case splitAtV i as of
( h, t ) -> ( a :. h, t )
at :: V n a -> Fin n -> a
v `at` fz@FZ = case fz of
( _ :: Fin (S m) )
| ( a :. _ ) <- v
-> a
v `at` fs@(FS j) = case fs of
( _ :: Fin (S m) )
| ( _ :. w ) <- v
-> w `at` j
lengthV :: V n a -> SNat n
lengthV Nil = SZ
lengthV (_ :. v) = SS (lengthV v)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment