{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Symantic.Typed.Lang where

import Data.Char (Char)
import Data.Bool (Bool(..))
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import qualified Data.Function as Fun

import Symantic.Typed.Derive

-- * Class 'Abstractable'
class Abstractable repr where
  -- | Application, aka. unabstract.
  (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (repr a -> repr b) -> repr (a->b)
  -- | Like 'lam' but whose argument is used only once,
  -- hence safe to beta-reduce (inline) without duplicating work.
  lam1 :: (repr a -> repr b) -> repr (a->b)
  const :: repr (a -> b -> a)
  flip :: repr ((a -> b -> c) -> b -> a -> c)
  id :: repr (a->a)
  (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
  ($) :: repr ((a->b) -> a -> b); infixr 0 $
  var :: repr a -> repr a
  (.@) = liftDerived2 (.@)
  lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
  const = liftDerived const
  flip = liftDerived flip
  id = liftDerived id
  (.) = liftDerived (.)
  ($) = liftDerived ($)
  var = liftDerived1 var
  default (.@) ::
    FromDerived2 Abstractable repr =>
    repr (a->b) -> repr a -> repr b
  default lam ::
    FromDerived Abstractable repr => Derivable repr =>
    (repr a -> repr b) -> repr (a->b)
  default lam1 ::
    FromDerived Abstractable repr => Derivable repr =>
    (repr a -> repr b) -> repr (a->b)
  default const ::
    FromDerived Abstractable repr =>
    repr (a -> b -> a)
  default flip ::
    FromDerived Abstractable repr =>
    repr ((a -> b -> c) -> b -> a -> c)
  default id ::
    FromDerived Abstractable repr =>
    repr (a->a)
  default (.) ::
    FromDerived Abstractable repr =>
    repr ((b->c) -> (a->b) -> a -> c)
  default ($) ::
    FromDerived Abstractable repr =>
    repr ((a->b) -> a -> b)
  default var ::
    FromDerived1 Abstractable repr =>
    repr a -> repr a

-- * Class 'Anythingable'
class Anythingable repr where
  anything :: repr a -> repr a
  anything = Fun.id

-- * Class 'Bottomable'
class Bottomable repr where
  bottom :: repr a

-- * Class 'Constantable'
class Constantable c repr where
  constant :: c -> repr c
  constant = liftDerived Fun.. constant
  default constant ::
    FromDerived (Constantable c) repr =>
    c -> repr c

bool :: Constantable Bool repr => Bool -> repr Bool
bool = constant @Bool
char :: Constantable Char repr => Char -> repr Char
char = constant @Char
unit :: Constantable () repr => repr ()
unit = constant @() ()

-- * Class 'Eitherable'
class Eitherable repr where
  left :: repr (l -> Either l r)
  right :: repr (r -> Either l r)
  left = liftDerived left
  right = liftDerived right
  default left ::
    FromDerived Eitherable repr =>
    repr (l -> Either l r)
  default right ::
    FromDerived Eitherable repr =>
    repr (r -> Either l r)

-- * Class 'Equalable'
class Equalable repr where
  equal :: Eq a => repr (a -> a -> Bool)
  equal = liftDerived equal
  default equal ::
    FromDerived Equalable repr =>
    Eq a => repr (a -> a -> Bool)

infix 4 `equal`, ==
(==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
(==) = lam (\x -> lam (\y -> equal .@ x .@ y))

-- * Class 'IfThenElseable'
class IfThenElseable repr where
  ifThenElse :: repr Bool -> repr a -> repr a -> repr a
  ifThenElse = liftDerived3 ifThenElse
  default ifThenElse ::
    FromDerived3 IfThenElseable repr =>
    repr Bool -> repr a -> repr a -> repr a

-- * Class 'Listable'
class Listable repr where
  cons :: repr (a -> [a] -> [a])
  nil :: repr [a]
  cons = liftDerived cons
  nil = liftDerived nil
  default cons ::
    FromDerived Listable repr =>
    repr (a -> [a] -> [a])
  default nil ::
    FromDerived Listable repr =>
    repr [a]

-- * Class 'Maybeable'
class Maybeable repr where
  nothing :: repr (Maybe a)
  just :: repr (a -> Maybe a)
  nothing = liftDerived nothing
  just = liftDerived just
  default nothing ::
    FromDerived Maybeable repr =>
    repr (Maybe a)
  default just ::
    FromDerived Maybeable repr =>
    repr (a -> Maybe a)