Main

Main.purs

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))