Sum.hs

{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, EmptyDataDecls,
  QuasiQuotes, UndecidableInstances, ScopedTypeVariables,
  MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances,
  FlexibleContexts #-}

{-# LANGUAGE TemplateHaskell #-}

{- |

Module      :  Type.Yoko.Sum
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Finite sums of types.

-}

module Type.Yoko.Sum ((:+), All(..), TSum, Exists(..), Elem) where

import Type.Yoko.Type
import Type.Yoko.Universe
import Data.Yoko.CoreTypes



infixr 5 :+
-- | Type-sum union. We re-use 'N' as type-sum singleton and 'V' as the empty
-- type-sum.
data t :+ s



-- | The higher-order universe @All@. @c@ inhabits @All u@ if @c@ is a type-sum
-- and all types in it inhabit @u@.
data All u c where
  SumV :: All u V
  SumN :: (t ::: u) => u t -> All u (N t)
  SumS :: All u c -> All u d -> All u (c :+ d)

instance V ::: All u where inhabits = SumV
instance (t ::: u) => N t ::: All u where inhabits = SumN inhabits
instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where
  inhabits = SumS inhabits inhabits

-- | @All 'NoneD'@ is satisfied by any type-sum.
type TSum = All NoneD





-- | The higher-order universe @Exists@. @c@ inhabits @Exists p@ if there
-- exists a type @t@ in the type-sum @c@ for which @'True' ~ 'Pred' p t@. NB
-- that @c@ is not necessarily a type-sum; i.e. there is no well-typed total
-- function from @Exists p c@ to @TSum c@.
data Exists p c where
  Here    :: p t        -> Exists p (N t)
  OnLeft  :: Exists p c -> Exists p (c :+ d)
  OnRight :: Exists p d -> Exists p (c :+ d)



data Nothing; data Just path

type family IsJust a
type instance IsJust Nothing = False
type instance IsJust (Just path) = True

type family Combine l r
type instance Combine Nothing Nothing = Nothing
type instance Combine Nothing (Just x) = Just (OnRight x)
type instance Combine (Just x) r = Just (OnLeft x)



data Here
data OnLeft x
data OnRight x

-- | @Elem t ts@ is 'True' if @t@ occurs in the type sum @ts@.
type Elem t ts = IsJust (Find ((:=:) t) ts)

type family Find (pred :: * -> *) c
type instance Find p (N t) = If (Pred p t) (Just Here) Nothing
type instance Find p (c :+ d) = Combine (Find p c) (Find p d)
type instance Find p V = Nothing



instance (Just path ~ Find p c, c ::: Exists p :? path) => c ::: Exists p where
  inhabits = inhabits_ [qP|path|]

instance (t ::: p)                => N t      ::: Exists p :? Here where
  inhabits = Anno $ Here inhabits
instance (c ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnLeft  path where
  inhabits = Anno $ OnLeft  (inhabits_ [qP|path|])
instance (d ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnRight path where
  inhabits = Anno $ OnRight (inhabits_ [qP|path|])