{-# 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
  (.@) = (Derived repr (a -> b) -> Derived repr a -> Derived repr b)
-> repr (a -> b) -> repr a -> repr b
forall (repr :: * -> *) a b c.
LiftDerived2 repr =>
(Derived repr a -> Derived repr b -> Derived repr c)
-> repr a -> repr b -> repr c
liftDerived2 Derived repr (a -> b) -> Derived repr a -> Derived repr b
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
(.@)
  lam repr a -> repr b
f = Derived repr (a -> b) -> repr (a -> b)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived ((Derived repr a -> Derived repr b) -> Derived repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (repr b -> Derived repr b
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive (repr b -> Derived repr b)
-> (Derived repr a -> repr b) -> Derived repr a -> Derived repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. repr a -> repr b
f (repr a -> repr b)
-> (Derived repr a -> repr a) -> Derived repr a -> repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Derived repr a -> repr a
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived))
  lam1 repr a -> repr b
f = Derived repr (a -> b) -> repr (a -> b)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived ((Derived repr a -> Derived repr b) -> Derived repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (repr b -> Derived repr b
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive (repr b -> Derived repr b)
-> (Derived repr a -> repr b) -> Derived repr a -> Derived repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. repr a -> repr b
f (repr a -> repr b)
-> (Derived repr a -> repr a) -> Derived repr a -> repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Derived repr a -> repr a
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived))
  const = Derived repr (a -> b -> a) -> repr (a -> b -> a)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (a -> b -> a)
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b -> a)
const
  flip = Derived repr ((a -> b -> c) -> b -> a -> c)
-> repr ((a -> b -> c) -> b -> a -> c)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr ((a -> b -> c) -> b -> a -> c)
forall (repr :: * -> *) a b c.
Abstractable repr =>
repr ((a -> b -> c) -> b -> a -> c)
flip
  id = Derived repr (a -> a) -> repr (a -> a)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (a -> a)
forall (repr :: * -> *) a. Abstractable repr => repr (a -> a)
id
  (.) = Derived repr ((b -> c) -> (a -> b) -> a -> c)
-> repr ((b -> c) -> (a -> b) -> a -> c)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr ((b -> c) -> (a -> b) -> a -> c)
forall (repr :: * -> *) b c a.
Abstractable repr =>
repr ((b -> c) -> (a -> b) -> a -> c)
(.)
  ($) = Derived repr ((a -> b) -> a -> b) -> repr ((a -> b) -> a -> b)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr ((a -> b) -> a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
repr ((a -> b) -> a -> b)
($)
  var = (Derived repr a -> Derived repr a) -> repr a -> repr a
forall (repr :: * -> *) a b.
LiftDerived1 repr =>
(Derived repr a -> Derived repr b) -> repr a -> repr b
liftDerived1 Derived repr a -> Derived repr a
forall (repr :: * -> *) a. Abstractable repr => repr a -> repr a
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 = repr a -> repr a
forall a. a -> a
Fun.id

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

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

bool :: Constantable Bool repr => Bool -> repr Bool
bool :: Bool -> repr Bool
bool = forall c (repr :: * -> *). Constantable c repr => c -> repr c
forall (repr :: * -> *).
Constantable Bool repr =>
Bool -> repr Bool
constant @Bool
char :: Constantable Char repr => Char -> repr Char
char :: Char -> repr Char
char = forall c (repr :: * -> *). Constantable c repr => c -> repr c
forall (repr :: * -> *).
Constantable Char repr =>
Char -> repr Char
constant @Char
unit :: Constantable () repr => repr ()
unit :: repr ()
unit = () -> repr ()
forall c (repr :: * -> *). Constantable c repr => c -> repr c
constant @() ()

-- * Class 'Eitherable'
class Eitherable repr where
  left :: repr (l -> Either l r)
  right :: repr (r -> Either l r)
  left = Derived repr (l -> Either l r) -> repr (l -> Either l r)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (l -> Either l r)
forall (repr :: * -> *) l r.
Eitherable repr =>
repr (l -> Either l r)
left
  right = Derived repr (r -> Either l r) -> repr (r -> Either l r)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (r -> Either l r)
forall (repr :: * -> *) r l.
Eitherable repr =>
repr (r -> Either l r)
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 = Derived repr (a -> a -> Bool) -> repr (a -> a -> Bool)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (a -> a -> Bool)
forall (repr :: * -> *) a.
(Equalable repr, Eq a) =>
repr (a -> a -> Bool)
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)
== :: repr (a -> a -> Bool)
(==) = (repr a -> repr (a -> Bool)) -> repr (a -> a -> Bool)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (\repr a
x -> (repr a -> repr Bool) -> repr (a -> Bool)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (\repr a
y -> repr (a -> a -> Bool)
forall (repr :: * -> *) a.
(Equalable repr, Eq a) =>
repr (a -> a -> Bool)
equal repr (a -> a -> Bool) -> repr a -> repr (a -> Bool)
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ repr a
x repr (a -> Bool) -> repr a -> repr Bool
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ repr a
y))

-- * Class 'IfThenElseable'
class IfThenElseable repr where
  ifThenElse :: repr Bool -> repr a -> repr a -> repr a
  ifThenElse = (Derived repr Bool
 -> Derived repr a -> Derived repr a -> Derived repr a)
-> repr Bool -> repr a -> repr a -> repr a
forall (repr :: * -> *) a b c d.
LiftDerived3 repr =>
(Derived repr a
 -> Derived repr b -> Derived repr c -> Derived repr d)
-> repr a -> repr b -> repr c -> repr d
liftDerived3 Derived repr Bool
-> Derived repr a -> Derived repr a -> Derived repr a
forall (repr :: * -> *) a.
IfThenElseable repr =>
repr Bool -> repr a -> repr a -> repr a
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 = Derived repr (a -> [a] -> [a]) -> repr (a -> [a] -> [a])
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (a -> [a] -> [a])
forall (repr :: * -> *) a. Listable repr => repr (a -> [a] -> [a])
cons
  nil = Derived repr [a] -> repr [a]
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr [a]
forall (repr :: * -> *) a. Listable repr => repr [a]
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 = Derived repr (Maybe a) -> repr (Maybe a)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (Maybe a)
forall (repr :: * -> *) a. Maybeable repr => repr (Maybe a)
nothing
  just = Derived repr (a -> Maybe a) -> repr (a -> Maybe a)
forall (repr :: * -> *) a.
LiftDerived repr =>
Derived repr a -> repr a
liftDerived Derived repr (a -> Maybe a)
forall (repr :: * -> *) a. Maybeable repr => repr (a -> Maybe a)
just
  default nothing ::
    FromDerived Maybeable repr =>
    repr (Maybe a)
  default just ::
    FromDerived Maybeable repr =>
    repr (a -> Maybe a)