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.Derive
  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 => Derivable repr =>
  50     (repr a -> repr b) -> repr (a->b)
  51   default lam1 ::
  52     FromDerived Abstractable repr => Derivable 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 'Bottomable'
  79 class Bottomable repr where
  80   bottom :: repr a
  81
  82 -- * Class 'Constantable'
  83 class Constantable c repr where
  84   constant :: c -> repr c
  85   constant = liftDerived Fun.. constant
  86   default constant ::
  87     FromDerived (Constantable c) repr =>
  88     c -> repr c
  89
  90 bool :: Constantable Bool repr => Bool -> repr Bool
  91 bool = constant @Bool
  92 char :: Constantable Char repr => Char -> repr Char
  93 char = constant @Char
  94 unit :: Constantable () repr => repr ()
  95 unit = constant @() ()
  96
  97 -- * Class 'Eitherable'
  98 class Eitherable repr where
  99   left :: repr (l -> Either l r)
 100   right :: repr (r -> Either l r)
 101   left = liftDerived left
 102   right = liftDerived right
 103   default left ::
 104     FromDerived Eitherable repr =>
 105     repr (l -> Either l r)
 106   default right ::
 107     FromDerived Eitherable repr =>
 108     repr (r -> Either l r)
 109
 110 -- * Class 'Equalable'
 111 class Equalable repr where
 112   equal :: Eq a => repr (a -> a -> Bool)
 113   equal = liftDerived equal
 114   default equal ::
 115     FromDerived Equalable repr =>
 116     Eq a => repr (a -> a -> Bool)
 117
 118 infix 4 `equal`, ==
 119 (==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
 120 (==) = lam (\x -> lam (\y -> equal .@ x .@ y))
 121
 122 -- * Class 'IfThenElseable'
 123 class IfThenElseable repr where
 124   ifThenElse :: repr Bool -> repr a -> repr a -> repr a
 125   ifThenElse = liftDerived3 ifThenElse
 126   default ifThenElse ::
 127     FromDerived3 IfThenElseable repr =>
 128     repr Bool -> repr a -> repr a -> repr a
 129
 130 -- * Class 'Listable'
 131 class Listable repr where
 132   cons :: repr (a -> [a] -> [a])
 133   nil :: repr [a]
 134   cons = liftDerived cons
 135   nil = liftDerived nil
 136   default cons ::
 137     FromDerived Listable repr =>
 138     repr (a -> [a] -> [a])
 139   default nil ::
 140     FromDerived Listable repr =>
 141     repr [a]
 142
 143 -- * Class 'Maybeable'
 144 class Maybeable repr where
 145   nothing :: repr (Maybe a)
 146   just :: repr (a -> Maybe a)
 147   nothing = liftDerived nothing
 148   just = liftDerived just
 149   default nothing ::
 150     FromDerived Maybeable repr =>
 151     repr (Maybe a)
 152   default just ::
 153     FromDerived Maybeable repr =>
 154     repr (a -> Maybe a)