Total language, work in progress

Total.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Total where

import Data.Function

infixr 7 :++:
infixr 6 :**:
infixr 5 :~~>:

data Lim = Mu | Nu

data Fu = K Ty | I | Fu :++: Fu | Fu :**: Fu | Ty :~~>: Fu

infixr 7 :+:
infixr 6 :*:
infixr 5 :~>:

data Ty = Ty :+: Ty | Ty :*: Ty | Ty :~>: Ty | Fix Lim Fu

class Apply (f :: Fu) (t :: Ty) (r :: Ty) | f t -> r

instance Apply (K ty1) ty2 ty1
instance Apply I ty ty
instance (Apply f1 ty ty1, Apply f2 ty ty2) => Apply (f1 :++: f2) ty (ty1 :+: ty2)
instance (Apply f1 ty ty1, Apply f2 ty ty2) => Apply (f1 :**: f2) ty (ty1 :*: ty2)
instance (Apply f ty ty2) => Apply (ty1 :~~>: f) ty (ty1 :~>: ty2)

infixr 0 <$>

class T repr where
  inl :: repr (ty1 :~>: ty1 :+: ty2)
  inr :: repr (ty2 :~>: ty1 :+: ty2)
  cas :: repr (ty1 :~>: r) -> repr (ty2 :~>: r) -> repr (ty1 :+: ty2 :~>: r)
  pi1 :: repr (ty1 :*: ty2 :~>: ty1)
  pi2 :: repr (ty1 :*: ty2 :~>: ty2)
  split :: repr (ty1 :~>: ty2 :~>: ty1 :*: ty2)
  lam :: (repr ty1 -> repr ty2) -> repr (ty1 :~>: ty2)
  (<$>) :: repr (ty1 :~>: ty2) -> repr ty1 -> repr ty2
  iin :: (Apply f (Fix l f) ffix) => repr (ffix :~>: Fix l f)
  out :: (Apply f (Fix l f) ffix) => repr (Fix l f :~>: ffix)
  cata :: (Apply f ty fty) => repr ((fty :~>: ty) :~>: Fix Mu f :~>: ty)
  ana :: (Apply f ty fty) => repr ((ty :~>: fty) :~>: ty :~>: Fix Nu f)
  
type Total a = forall repr. (T repr) => repr a

data Impl ty where
  Sum :: Either (Impl ty1) (Impl ty2) -> Impl (ty1 :+: ty2)
  Prod :: (Impl ty1, Impl ty2) -> Impl (ty1 :*: ty2)
  Arr :: (Impl ty1 -> Impl ty2) -> Impl (ty1 :~>: ty2)
  Rec :: (Apply f (Fix l f) r) => Impl r -> Impl (Fix l f)
  
hmap = undefined
  
instance T Impl where
  inl = Arr $ Sum . Left
  inr = Arr $ Sum . Right
  cas (Arr f) (Arr g) = Arr $ \(Sum e) -> either f g e
  pi1 = Arr $ \(Prod (x, _)) -> x
  pi2 = Arr $ \(Prod (_, y)) -> y
  split = Arr $ \x -> Arr $ \y -> Prod (x, y)
  lam = Arr
  (Arr f) <$> x = f x
  iin = Arr Rec
  --out = Arr $ \(Rec x) -> x
  cata = Arr $ \phi@(Arr f) -> fix $ \cata' -> Arr $ \(Rec x) -> f $ hmap cata' $ x
  --ana = Arr $ \psi@(Arr f) -> fix $ \ana' -> Arr $ \x -> Rec $ hmap ana' $ f x

eval :: Total a -> Impl a
eval x = x
  
infixr 3 <.>

(<.>) :: (T repr) => repr (b :~>: c) -> repr (a :~>: b) -> repr (a :~>: c)
f <.> g = lam $ \x -> f <$> g <$> x

type Void = Fix Mu I

absurd :: Total (Void :~>: a)
absurd = cata <$> (lam id)

type Unit = Void :~>: Void

unique :: Total Unit
unique = lam id

type Nat = Fix Mu (K Unit :++: I)

zero :: Total Nat
zero = iin <$> inl <$> unique

succ' :: Total (Nat :~>: Nat)
succ' = iin <.> inr

pred' :: Total (Nat :~>: Nat)
pred' = cas (lam $ const zero) (lam id) <.> out