More fiddling with Extendible types, Type functions, Pattern Synonyms etc.

Object.hs

{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
module Object where

import Data.Singletons
import Data.Singletons.Prelude.Base
import Data.Void


data Extendable (tf :: TyFun chPK (TyFun myPK * -> *) -> *)
                (chP :: chPK)
                (myP :: myPK)
                (myO :: *) =
  Extendable { _required :: tf @@ chP @@ myP
             , _optional :: myO
             }
  -- deriving (Show,Read,Eq,Ord)


--- TODO : For some reason we cannot derive this anymore
instance (Show (f @@ chP @@ myP), Show o) =>
         Show (Extendable f chP myP o) where
  show (r :+ o) = concat [ show r , " :+ ", show o ]

instance Read (Extendable f chP p o)
instance Eq (Extendable f chP p o)
instance Ord (Extendable f chP p o)





-- data Extendable (tf :: TyFun kp * -> *) (p :: kp) (o :: *) =
--   Extendable { _required :: tf @@ p
--              , _optional :: o
--              }
--   deriving (Show,Read,Eq,Ord)


type ConstructorExtendible (tc :: chPK -> myPK -> *) (chP :: chPK) (myP :: myPK) (o :: *) =
  Extendable (TyCon2 tc) chP myP o



-- const' a b = b

--  We revert the order of the parameters so we can make SimpleExtendable a functor

newtype SimpleExtendable (o :: *) (r :: *) =
  Simple { unSimple :: Extendable ConstSym0 r Void o }
  deriving (Show,Read,Eq,Ord)
-- Note : we want a reversed Const: one that ignores the first argument and returns
-- the second. So we reverse the child and my own parmeters to do this


class ExtractExt c where
  type Required c
  type Optional c

  extractValues :: c -> (Required c, Optional c)







instance ExtractExt (Extendable c chP p o) where
  type Required (Extendable c chP p o) = c @@ chP @@ p
  type Optional (Extendable c chP p o) = o
  extractValues (Extendable r o) = (r,o)

-- instance ExtractExt (SimpleExtendable o r)  where
--   type Required (SimpleExtendable o r) = r
--   type Optional (SimpleExtendable o r) = o
--   extractValues = extractValues . unSimple

pattern r :+ o <- (extractValues -> (r,o))
pattern r :<+ o = Simple (Extendable r o)




extendableStr = "foo" :<+ ()




newtype Point2 r = Point2 (r,r)
                 deriving (Show,Read,Eq,Ord)

pattern Point x y = Point2 (x,y)


data Color = Red | Blue | Green deriving (Show,Read,Eq,Ord)


redP = Point 0 0 :<+ Red

blueP = Point 1 1 :<+ Blue

pts = [redP, blueP]

type r :<+ o = SimpleExtendable o r



newtype Polygon o r = Polygon [Point2 r :<+ o]
                    deriving (Show,Read,Eq,Ord)


-- degen :: Polygon Integer ()
degen = Polygon []

-- myPoly :: Polygon Integer Color
myPoly = Polygon pts



-- type EXT chO myO myC r = ConstructorExtendible myC r myO

-- redPoly :: ConstructorExtendible Polygon o r Color
bluePoly :: ConstructorExtendible Polygon () Integer Color
bluePoly = Extendable degen Blue

-- redDegen :: SimpleExtendable Color (Polygon Integer ())
redDegen = degen :<+ Red

-- -- type PolygonSym = TyFun (*,*) * -> *


-- -- type ConstructorExtendible2 (tc :: k1 -> k2 -> *) (t :: (k1,k2)) o =
-- --   Extendable

-- --extDegen :: ConstructorExtendible (Polygon Integer) () Color

-- extDegen = Extendable degen Red