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 Listable repr where
 107   cons :: repr (a -> [a] -> [a])
 108   nil :: repr [a]
 109   default cons ::
 110     Liftable repr => Listable (Output repr) =>
 111     repr (a -> [a] -> [a])
 112   default nil ::
 113     Liftable repr => Listable (Output repr) =>
 114     repr [a]
 115   cons = lift cons
 116   nil = lift nil
 117 class Maybeable repr where
 118   nothing :: repr (Maybe a)
 119   just :: repr (a -> Maybe a)
 120   default nothing ::
 121     Liftable repr => Maybeable (Output repr) =>
 122     repr (Maybe a)
 123   default just ::
 124     Liftable repr => Maybeable (Output repr) =>
 125     repr (a -> Maybe a)
 126   nothing = lift nothing
 127   just = lift just