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.Trans
  20
  21 class Abstractable repr where
  22   -- | Application, aka. unabstract.
  23   (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
  24   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  25   lam :: (repr a -> repr b) -> repr (a->b)
  26   -- | Like 'lam' but whose argument is used only once,
  27   -- hence safe to beta-reduce (inline) without duplicating work.
  28   lam1 :: (repr a -> repr b) -> repr (a->b)
  29   const :: repr (a -> b -> a)
  30   flip :: repr ((a -> b -> c) -> b -> a -> c)
  31   id :: repr (a->a)
  32   (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
  33   ($) :: repr ((a->b) -> a -> b); infixr 0 $
  34   var :: repr a -> repr a
  35   default (.@) ::
  36     Liftable2 repr => Abstractable (Output repr) =>
  37     repr (a->b) -> repr a -> repr b
  38   default lam ::
  39     Liftable repr => Unliftable repr => Abstractable (Output repr) =>
  40     (repr a -> repr b) -> repr (a->b)
  41   default lam1 ::
  42     Liftable repr => Unliftable repr => Abstractable (Output repr) =>
  43     (repr a -> repr b) -> repr (a->b)
  44   default const ::
  45     Liftable repr => Abstractable (Output repr) =>
  46     repr (a -> b -> a)
  47   default flip ::
  48     Liftable repr => Abstractable (Output repr) =>
  49     repr ((a -> b -> c) -> b -> a -> c)
  50   default id ::
  51     Liftable repr => Abstractable (Output repr) =>
  52     repr (a->a)
  53   default (.) ::
  54     Liftable repr => Abstractable (Output repr) =>
  55     repr ((b->c) -> (a->b) -> a -> c)
  56   default ($) ::
  57     Liftable repr => Abstractable (Output repr) =>
  58     repr ((a->b) -> a -> b)
  59   default var ::
  60     Liftable1 repr => Abstractable (Output repr) =>
  61     repr a -> repr a
  62   (.@) = lift2 (.@)
  63   lam f = lift (lam (trans Fun.. f Fun.. trans))
  64   lam1 f = lift (lam1 (trans Fun.. f Fun.. trans))
  65   const = lift const
  66   flip = lift flip
  67   id = lift id
  68   (.) = lift (.)
  69   ($) = lift ($)
  70   var = lift1 var
  71 class Anythingable repr where
  72   anything :: repr a -> repr a
  73   anything = Fun.id
  74 class Constantable c repr where
  75   constant :: c -> repr c
  76   default constant ::
  77     Liftable repr => Constantable c (Output repr) =>
  78     c -> repr c
  79   constant = lift Fun.. constant
  80 bool :: Constantable Bool repr => Bool -> repr Bool
  81 bool = constant @Bool
  82 char :: Constantable Char repr => Char -> repr Char
  83 char = constant @Char
  84 unit :: Constantable () repr => repr ()
  85 unit = constant @() ()
  86 class Eitherable repr where
  87   left :: repr (l -> Either l r)
  88   right :: repr (r -> Either l r)
  89   default left ::
  90     Liftable repr => Eitherable (Output repr) =>
  91     repr (l -> Either l r)
  92   default right ::
  93     Liftable repr => Eitherable (Output repr) =>
  94     repr (r -> Either l r)
  95   left = lift left
  96   right = lift right
  97 class Equalable repr where
  98   equal :: Eq a => repr (a -> a -> Bool)
  99   default equal ::
 100     Liftable repr => Equalable (Output repr) =>
 101     Eq a => repr (a -> a -> Bool)
 102   equal = lift equal
 103 infix 4 `equal`, ==
 104 (==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
 105 (==) = lam (\x -> lam (\y -> equal .@ x .@ y))
 106 class IfThenElseable repr where
 107   ifThenElse :: repr Bool -> repr a -> repr a -> repr a
 108   default ifThenElse ::
 109     Liftable3 repr => IfThenElseable (Output repr) =>
 110     repr Bool -> repr a -> repr a -> repr a
 111   ifThenElse = lift3 ifThenElse
 112 class Listable repr where
 113   cons :: repr (a -> [a] -> [a])
 114   nil :: repr [a]
 115   default cons ::
 116     Liftable repr => Listable (Output repr) =>
 117     repr (a -> [a] -> [a])
 118   default nil ::
 119     Liftable repr => Listable (Output repr) =>
 120     repr [a]
 121   cons = lift cons
 122   nil = lift nil
 123 class Maybeable repr where
 124   nothing :: repr (Maybe a)
 125   just :: repr (a -> Maybe a)
 126   default nothing ::
 127     Liftable repr => Maybeable (Output repr) =>
 128     repr (Maybe a)
 129   default just ::
 130     Liftable repr => Maybeable (Output repr) =>
 131     repr (a -> Maybe a)
 132   nothing = lift nothing
 133   just = lift just