-- An example to show how we could implement GHC-style Generics using
-- functional dependencies.
--
-- See https://hackage.haskell.org/package/base-4.9.0.0/docs/GHC-Generics.html

module Main where

import Prelude
import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (CONSOLE, log, logShow)

-- Representation for types with no constructors
data V1

-- Representation for constructors with no arguments
data U1 = U1

-- Representation for sum types
data Sum a b = Inl a | Inr b

infixr 5 type Sum as +

-- Representation for product types
data Product a b = Product a b

infixr 6 type Product as *

-- Representation for data constructors, with the data constructor name indicated
-- at the type level.
data Ctor (name :: Symbol) a = Ctor a

-- Representation for occurrences of other types in a data type definition.
data K a = K a

-- The Generic class asserts the existence of a type function from "real" types
-- to representation types, and an isomorphism between them.
class Generic a repr | a -> repr where
  to :: a -> repr
  from :: repr -> a

-- We can write an instance for the (recursive) type of lists. Note that these
-- instances would be generated by the compiler ideally.
data List a = Nil | Cons a (List a)

instance genericList :: Generic (List a) (Ctor "Nil" U1 + Ctor "Cons" (K a * K (List a))) where
  to Nil = Inl (Ctor U1)
  to (Cons x xs) = Inr (Ctor (Product (K x) (K xs)))
  from (Inl (Ctor U1)) = Nil
  from (Inr (Ctor (Product (K x) (K xs)))) = Cons x xs

-- We'd like to refect type level strings (for data constructor names) at the value
-- level, so that we can "show" them. Again, these instances would ideally be derived
-- for us.
class KnownSymbol (sym :: Symbol) where
  symbol :: forall proxy. proxy sym -> String

instance knownSymbolNil :: KnownSymbol "Nil" where
  symbol _ = "Nil"

instance knownSymbolCons :: KnownSymbol "Cons" where
  symbol _ = "Cons"

-- A proxy for a type-level string.
data SProxy (sym :: Symbol) = SProxy

-- To write generic functions, we create a corresponding type class, and use the
-- type class machinery to infer the correct function based on the representation
-- type.
class GShow a where
  gShow :: a -> String

-- Now provide instances for GShow for the appropriate representation types.
-- Note: we don't have to implement all instances here.

instance gShowU1 :: GShow U1 where
  gShow _ = ""

instance gShowSum :: (GShow a, GShow b) => GShow (a + b) where
  gShow (Inl a) = gShow a
  gShow (Inr b) = gShow b

instance gShowProduct :: (GShow a, GShow b) => GShow (a * b) where
  gShow (Product a b) = gShow a <> gShow b

instance gShowCtor :: (KnownSymbol ctor, GShow a) => GShow (Ctor ctor a) where
  gShow (Ctor a) = "(" <> symbol (SProxy :: SProxy ctor) <> gShow a <> ")"

instance gShowK :: Show a => GShow (K a) where
  gShow (K a) = " " <> show a

-- Now we can implement a generic show function which uses the GShow instance
-- on the representation type.
genericShow :: forall a repr. (Generic a repr, GShow repr) => a -> String
genericShow x = gShow (to x)

-- Note how the required instance here is Show a, and not Generic a.
-- This allows us to use generic programming on a wider variety of types
-- (including types which contain foreign types) than we can use now.
instance showList :: Show a => Show (List a) where
  show xs = genericShow xs -- (we need to eta expand here to avoid stack overflow
                           -- due to recursion implicit in the instance lookup)

-- Another example: Eq

class GEq a where
  gEq :: a -> a -> Boolean

instance gEqU1 :: GEq U1 where
  gEq _ _ = true

instance gEqSum :: (GEq a, GEq b) => GEq (a + b) where
  gEq (Inl a1) (Inl a2) = gEq a1 a2
  gEq (Inr b1) (Inr b2) = gEq b1 b2
  gEq _ _ = false

instance gEqProduct :: (GEq a, GEq b) => GEq (a * b) where
  gEq (Product a1 b1) (Product a2 b2) = gEq a1 a2 && gEq b1 b2

instance gEqCtor :: (KnownSymbol ctor, GEq a) => GEq (Ctor ctor a) where
  gEq (Ctor a1) (Ctor a2) = gEq a1 a2

instance gEqK :: Eq a => GEq (K a) where
  gEq (K a1) (K a2) = a1 == a2

genericEq :: forall a repr. (Generic a repr, GEq repr) => a -> a -> Boolean
genericEq x y = gEq (to x) (to y)

instance eqList :: Eq a => Eq (List a) where
  eq xs ys = genericEq xs ys

main :: Eff (console :: CONSOLE) Unit
main = do
  logShow (Cons 1 Nil)
  logShow (Cons 1 (Cons 2 Nil))
  logShow (Cons 'x' (Cons 'y' (Cons 'z' Nil)))

  logShow (Cons 1 (Cons 2 Nil) == Cons 1 (Cons 2 Nil))
  logShow (Cons 1 (Cons 2 Nil) == Cons 1 Nil)

  log "Done"