Skip to content

Instantly share code, notes, and snippets.

@xgrommx
Created July 7, 2021 23:11
Show Gist options
  • Save xgrommx/3a6c948a3564f90fde29f998b01dfc7b to your computer and use it in GitHub Desktop.
Save xgrommx/3a6c948a3564f90fde29f998b01dfc7b to your computer and use it in GitHub Desktop.
Main
module Main where
import Prelude
import Type.Proxy
import Type.Data.Peano as Peano
type TypeExpr :: forall k. k -> Type
type TypeExpr a = Proxy a -> Type
class TEval :: forall a. TypeExpr a -> a -> Constraint
class TEval expr result | expr -> result
proxyEval :: forall expr ty. TEval expr ty => Proxy expr -> Proxy ty
proxyEval _ = Proxy
foreign import data TProject :: forall f t. t -> TypeExpr (f t)
foreign import data FMap :: forall f a b. (a -> TypeExpr b) -> f a -> TypeExpr (f b)
foreign import data Cata :: forall t f a. (f a -> TypeExpr a) -> t -> TypeExpr a
instance (TEval (TProject x) p, TEval (FMap (Cata alg) p) c, TEval (alg c) r) => TEval (Cata alg x) r
data TList :: forall k. k -> Type
data TList a
foreign import data TNil :: forall k. TList k
foreign import data TCons :: forall k. k -> TList k -> TList k
infixr 1 type TCons as :>
data TListF :: forall m k. m -> k -> Type
data TListF a b
foreign import data TNilF :: forall m k. TListF m k
foreign import data TConsF :: forall m k. m -> k -> TListF m k
infixr 1 type TConsF as ::>
instance TEval (FMap f TNilF) TNilF
instance TEval (f b) b' => TEval (FMap f (TConsF a b)) (TConsF a b')
instance TEval (TProject TNil) TNilF
instance TEval (TProject (TCons x xs)) (TConsF x xs)
foreign import data LengthAlg :: forall a. TListF a Peano.Int -> TypeExpr Peano.Int
instance TEval (LengthAlg TNilF) Peano.P0
instance (Peano.SumInt b Peano.P1 c) => TEval (LengthAlg (TConsF a b)) c
foreign import data Length :: forall a. TList a -> TypeExpr Peano.Int
instance (TEval (Cata (LengthAlg :: TListF a Peano.Int -> TypeExpr Peano.Int) t) r) => TEval (Length ((t) :: TList a)) r
type V0 :: TList Type
type V0 = Int :> Number :> TNil
type V1 :: TList Peano.Int
type V1 = Peano.P30 :> Peano.P9 :> Peano.P20 :> Peano.P0 :> TNil
e1 :: Proxy Peano.P2
e1 = proxyEval (Proxy :: _ (Length V0))
e2 :: Proxy Peano.P4
e2 = proxyEval (Proxy :: _ (Length V1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment