src/Symantic/Typed/Lang.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE NoMonomorphismRestriction #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeApplications #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE NoImplicitPrelude #-}
  10 module Symantic.Typed.Lang where
  11
  12 import Data.Char (Char)
  13 import Data.Bool (Bool(..))
  14 import Data.Either (Either(..))
  15 import Data.Eq (Eq)
  16 import Data.Maybe (Maybe(..))
  17 import qualified Data.Function as Fun
  18
  19 import Symantic.Typed.Transformable
  20
  21 -- * Class 'Abstractable'
  22 class Abstractable repr where
  23   -- | Application, aka. unabstract.
  24   (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
  25   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  26   lam :: (repr a -> repr b) -> repr (a->b)
  27   -- | Like 'lam' but whose argument is used only once,
  28   -- hence safe to beta-reduce (inline) without duplicating work.
  29   lam1 :: (repr a -> repr b) -> repr (a->b)
  30   const :: repr (a -> b -> a)
  31   flip :: repr ((a -> b -> c) -> b -> a -> c)
  32   id :: repr (a->a)
  33   (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
  34   ($) :: repr ((a->b) -> a -> b); infixr 0 $
  35   var :: repr a -> repr a
  36   (.@) = liftDerived2 (.@)
  37   lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
  38   lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
  39   const = liftDerived const
  40   flip = liftDerived flip
  41   id = liftDerived id
  42   (.) = liftDerived (.)
  43   ($) = liftDerived ($)
  44   var = liftDerived1 var
  45   default (.@) ::
  46     FromDerived2 Abstractable repr =>
  47     repr (a->b) -> repr a -> repr b
  48   default lam ::
  49     FromDerived Abstractable repr => Derive repr =>
  50     (repr a -> repr b) -> repr (a->b)
  51   default lam1 ::
  52     FromDerived Abstractable repr => Derive repr =>
  53     (repr a -> repr b) -> repr (a->b)
  54   default const ::
  55     FromDerived Abstractable repr =>
  56     repr (a -> b -> a)
  57   default flip ::
  58     FromDerived Abstractable repr =>
  59     repr ((a -> b -> c) -> b -> a -> c)
  60   default id ::
  61     FromDerived Abstractable repr =>
  62     repr (a->a)
  63   default (.) ::
  64     FromDerived Abstractable repr =>
  65     repr ((b->c) -> (a->b) -> a -> c)
  66   default ($) ::
  67     FromDerived Abstractable repr =>
  68     repr ((a->b) -> a -> b)
  69   default var ::
  70     FromDerived1 Abstractable repr =>
  71     repr a -> repr a
  72
  73 -- * Class 'Anythingable'
  74 class Anythingable repr where
  75   anything :: repr a -> repr a
  76   anything = Fun.id
  77
  78 -- * Class 'Constantable'
  79 class Constantable c repr where
  80   constant :: c -> repr c
  81   constant = liftDerived Fun.. constant
  82   default constant ::
  83     FromDerived (Constantable c) repr =>
  84     c -> repr c
  85
  86 bool :: Constantable Bool repr => Bool -> repr Bool
  87 bool = constant @Bool
  88 char :: Constantable Char repr => Char -> repr Char
  89 char = constant @Char
  90 unit :: Constantable () repr => repr ()
  91 unit = constant @() ()
  92
  93 -- * Class 'Eitherable'
  94 class Eitherable repr where
  95   left :: repr (l -> Either l r)
  96   right :: repr (r -> Either l r)
  97   left = liftDerived left
  98   right = liftDerived right
  99   default left ::
 100     FromDerived Eitherable repr =>
 101     repr (l -> Either l r)
 102   default right ::
 103     FromDerived Eitherable repr =>
 104     repr (r -> Either l r)
 105
 106 -- * Class 'Equalable'
 107 class Equalable repr where
 108   equal :: Eq a => repr (a -> a -> Bool)
 109   equal = liftDerived equal
 110   default equal ::
 111     FromDerived Equalable repr =>
 112     Eq a => repr (a -> a -> Bool)
 113
 114 infix 4 `equal`, ==
 115 (==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
 116 (==) = lam (\x -> lam (\y -> equal .@ x .@ y))
 117
 118 -- * Class 'IfThenElseable'
 119 class IfThenElseable repr where
 120   ifThenElse :: repr Bool -> repr a -> repr a -> repr a
 121   ifThenElse = liftDerived3 ifThenElse
 122   default ifThenElse ::
 123     FromDerived3 IfThenElseable repr =>
 124     repr Bool -> repr a -> repr a -> repr a
 125
 126 -- * Class 'Listable'
 127 class Listable repr where
 128   cons :: repr (a -> [a] -> [a])
 129   nil :: repr [a]
 130   cons = liftDerived cons
 131   nil = liftDerived nil
 132   default cons ::
 133     FromDerived Listable repr =>
 134     repr (a -> [a] -> [a])
 135   default nil ::
 136     FromDerived Listable repr =>
 137     repr [a]
 138
 139 -- * Class 'Maybeable'
 140 class Maybeable repr where
 141   nothing :: repr (Maybe a)
 142   just :: repr (a -> Maybe a)
 143   nothing = liftDerived nothing
 144   just = liftDerived just
 145   default nothing ::
 146     FromDerived Maybeable repr =>
 147     repr (Maybe a)
 148   default just ::
 149     FromDerived Maybeable repr =>
 150     repr (a -> Maybe a)