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