src/Symantic/Lang.hs

   1 {-# LANGUAGE DataKinds #-} -- For ReprKind
   2 {-# LANGUAGE PatternSynonyms #-} -- For (:!:)
   3 {-# LANGUAGE TypeFamilyDependencies #-} -- For Permutation
   4 {-# LANGUAGE UndecidableInstances #-} -- For Permutation
   5 module Symantic.Lang where
   6
   7 import Data.Bool (Bool(..))
   8 import Data.Char (Char)
   9 import Data.Either (Either(..))
  10 import Data.Eq (Eq)
  11 import Data.Kind (Type)
  12 import Data.Maybe (Maybe(..), fromJust)
  13 import Data.Proxy (Proxy(..))
  14 import GHC.Generics (Generic)
  15 import qualified Control.Category as Cat
  16 import qualified Data.Function as Fun
  17 import qualified Data.Tuple as Tuple
  18
  19 import Symantic.Derive
  20 import Symantic.ADT
  21 import Symantic.CurryN
  22
  23 -- * Type 'ReprKind'
  24 type ReprKind = Type -> Type
  25
  26 -- * Class 'Abstractable'
  27 class Abstractable repr where
  28   -- | Application, aka. unabstract.
  29   (.@) :: repr (a->b) -> repr a -> repr b; infixl 9 .@
  30   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  31   lam :: (repr a -> repr b) -> repr (a->b)
  32   -- | Like 'lam' but whose argument is used only once,
  33   -- hence safe to beta-reduce (inline) without duplicating work.
  34   lam1 :: (repr a -> repr b) -> repr (a->b)
  35   const :: repr (a -> b -> a)
  36   flip :: repr ((a -> b -> c) -> b -> a -> c)
  37   id :: repr (a->a)
  38   (.) :: repr ((b->c) -> (a->b) -> a -> c); infixr 9 .
  39   ($) :: repr ((a->b) -> a -> b); infixr 0 $
  40   var :: repr a -> repr a
  41   (.@) = liftDerived2 (.@)
  42   lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
  43   lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
  44   const = liftDerived const
  45   flip = liftDerived flip
  46   id = liftDerived id
  47   (.) = liftDerived (.)
  48   ($) = liftDerived ($)
  49   var = liftDerived1 var
  50   default (.@) ::
  51     FromDerived2 Abstractable repr =>
  52     repr (a->b) -> repr a -> repr b
  53   default lam ::
  54     FromDerived Abstractable repr => Derivable repr =>
  55     (repr a -> repr b) -> repr (a->b)
  56   default lam1 ::
  57     FromDerived Abstractable repr => Derivable repr =>
  58     (repr a -> repr b) -> repr (a->b)
  59   default const ::
  60     FromDerived Abstractable repr =>
  61     repr (a -> b -> a)
  62   default flip ::
  63     FromDerived Abstractable repr =>
  64     repr ((a -> b -> c) -> b -> a -> c)
  65   default id ::
  66     FromDerived Abstractable repr =>
  67     repr (a->a)
  68   default (.) ::
  69     FromDerived Abstractable repr =>
  70     repr ((b->c) -> (a->b) -> a -> c)
  71   default ($) ::
  72     FromDerived Abstractable repr =>
  73     repr ((a->b) -> a -> b)
  74   default var ::
  75     FromDerived1 Abstractable repr =>
  76     repr a -> repr a
  77
  78 -- * Class 'Anythingable'
  79 class Anythingable repr where
  80   anything :: repr a -> repr a
  81   anything = Fun.id
  82
  83 -- * Class 'Bottomable'
  84 class Bottomable repr where
  85   bottom :: repr a
  86
  87 -- * Class 'Constantable'
  88 class Constantable c repr where
  89   constant :: c -> repr c
  90   constant = liftDerived Fun.. constant
  91   default constant ::
  92     FromDerived (Constantable c) repr =>
  93     c -> repr c
  94
  95 bool :: Constantable Bool repr => Bool -> repr Bool
  96 bool = constant @Bool
  97 char :: Constantable Char repr => Char -> repr Char
  98 char = constant @Char
  99 unit :: Constantable () repr => repr ()
 100 unit = constant @() ()
 101
 102 -- * Class 'Eitherable'
 103 class Eitherable repr where
 104   left :: repr (l -> Either l r)
 105   right :: repr (r -> Either l r)
 106   left = liftDerived left
 107   right = liftDerived right
 108   default left ::
 109     FromDerived Eitherable repr =>
 110     repr (l -> Either l r)
 111   default right ::
 112     FromDerived Eitherable repr =>
 113     repr (r -> Either l r)
 114
 115 -- * Class 'Equalable'
 116 class Equalable repr where
 117   equal :: Eq a => repr (a -> a -> Bool)
 118   equal = liftDerived equal
 119   default equal ::
 120     FromDerived Equalable repr =>
 121     Eq a => repr (a -> a -> Bool)
 122
 123 infix 4 `equal`, ==
 124 (==) :: (Abstractable repr, Equalable repr, Eq a) => repr (a -> a -> Bool)
 125 (==) = lam (\x -> lam (\y -> equal .@ x .@ y))
 126
 127 -- * Class 'IfThenElseable'
 128 class IfThenElseable repr where
 129   ifThenElse :: repr Bool -> repr a -> repr a -> repr a
 130   ifThenElse = liftDerived3 ifThenElse
 131   default ifThenElse ::
 132     FromDerived3 IfThenElseable repr =>
 133     repr Bool -> repr a -> repr a -> repr a
 134
 135 -- * Class 'Listable'
 136 class Listable repr where
 137   cons :: repr (a -> [a] -> [a])
 138   nil :: repr [a]
 139   cons = liftDerived cons
 140   nil = liftDerived nil
 141   default cons ::
 142     FromDerived Listable repr =>
 143     repr (a -> [a] -> [a])
 144   default nil ::
 145     FromDerived Listable repr =>
 146     repr [a]
 147
 148 -- * Class 'Maybeable'
 149 class Maybeable repr where
 150   nothing :: repr (Maybe a)
 151   just :: repr (a -> Maybe a)
 152   nothing = liftDerived nothing
 153   just = liftDerived just
 154   default nothing ::
 155     FromDerived Maybeable repr =>
 156     repr (Maybe a)
 157   default just ::
 158     FromDerived Maybeable repr =>
 159     repr (a -> Maybe a)
 160
 161 -- * Class 'IsoFunctor'
 162 class IsoFunctor repr where
 163   (<%>) :: Iso a b -> repr a -> repr b; infixl 4 <%>
 164   (<%>) iso = liftDerived1 (iso <%>)
 165   default (<%>) ::
 166     FromDerived1 IsoFunctor repr =>
 167     Iso a b -> repr a -> repr b
 168
 169 -- ** Type 'Iso'
 170 data Iso a b = Iso { a2b :: a->b, b2a :: b->a }
 171 instance Cat.Category Iso where
 172   id = Iso Cat.id Cat.id
 173   f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
 174
 175 -- * Class 'ProductFunctor'
 176 -- | Beware that this is an @infixr@,
 177 -- not @infixl@ like to 'Control.Applicative.<*>';
 178 -- this is to follow what is expected by 'ADT'.
 179 class ProductFunctor repr where
 180   (<.>) :: repr a -> repr b -> repr (a, b); infixr 4 <.>
 181   (<.>) = liftDerived2 (<.>)
 182   default (<.>) ::
 183     FromDerived2 ProductFunctor repr =>
 184     repr a -> repr b -> repr (a, b)
 185   (<.) :: repr a -> repr () -> repr a; infixr 4 <.
 186   ra <. rb = Iso Tuple.fst (, ()) <%> (ra <.> rb)
 187   default (<.) :: IsoFunctor repr => repr a -> repr () -> repr a
 188   (.>) :: repr () -> repr a -> repr a; infixr 4 .>
 189   ra .> rb = Iso Tuple.snd (() ,) <%> (ra <.> rb)
 190   default (.>) :: IsoFunctor repr => repr () -> repr a -> repr a
 191
 192 -- * Class 'SumFunctor'
 193 -- | Beware that this is an @infixr@,
 194 -- not @infixl@ like to 'Control.Applicative.<|>';
 195 -- this is to follow what is expected by 'ADT'.
 196 class SumFunctor repr where
 197   (<+>) :: repr a -> repr b -> repr (Either a b); infixr 3 <+>
 198   (<+>) = liftDerived2 (<+>)
 199   default (<+>) ::
 200     FromDerived2 SumFunctor repr =>
 201     repr a -> repr b -> repr (Either a b)
 202
 203 -- * Class 'AlternativeFunctor'
 204 -- | Beware that this is an @infixr@,
 205 -- not @infixl@ like to 'Control.Applicative.<|>';
 206 -- this is to follow what is expected by 'ADT'.
 207 class AlternativeFunctor repr where
 208   (<|>) :: repr a -> repr a -> repr a; infixr 3 <|>
 209   (<|>) = liftDerived2 (<|>)
 210   default (<|>) ::
 211     FromDerived2 AlternativeFunctor repr =>
 212     repr a -> repr a -> repr a
 213
 214 -- * Class 'Dicurryable'
 215 class Dicurryable repr where
 216   dicurry ::
 217     CurryN args =>
 218     proxy args ->
 219     (args-..->a) -> -- construction
 220     (a->Tuples args) -> -- destruction
 221     repr (Tuples args) ->
 222     repr a
 223   dicurry args constr destr = liftDerived1 (dicurry args constr destr)
 224   default dicurry ::
 225     FromDerived1 Dicurryable repr =>
 226     CurryN args =>
 227     proxy args ->
 228     (args-..->a) ->
 229     (a->Tuples args) ->
 230     repr (Tuples args) ->
 231     repr a
 232
 233 construct ::
 234   forall args a repr.
 235   Dicurryable repr =>
 236   Generic a =>
 237   EoTOfRep a =>
 238   CurryN args =>
 239   Tuples args ~ EoT (ADT a) =>
 240   (args ~ Args (args-..->a)) =>
 241   (args-..->a) ->
 242   repr (Tuples args) ->
 243   repr a
 244 construct f = dicurry (Proxy::Proxy args) f eotOfadt
 245
 246 adt ::
 247   forall adt repr.
 248   IsoFunctor repr =>
 249   Generic adt =>
 250   RepOfEoT adt =>
 251   EoTOfRep adt =>
 252   repr (EoT (ADT adt)) ->
 253   repr adt
 254 adt = (<%>) (Iso adtOfeot eotOfadt)
 255
 256 -- ** Class 'Emptyable'
 257 class Emptyable repr where
 258   empty :: repr a
 259   empty = liftDerived empty
 260   default empty ::
 261     FromDerived Emptyable repr =>
 262     repr a
 263
 264 -- ** Class 'Optionable'
 265 class Optionable repr where
 266   option :: repr a -> repr a
 267   optional :: repr a -> repr (Maybe a)
 268   option = liftDerived1 option
 269   optional = liftDerived1 optional
 270   default option ::
 271     FromDerived1 Optionable repr =>
 272     repr a -> repr a
 273   default optional ::
 274     FromDerived1 Optionable repr =>
 275     repr a -> repr (Maybe a)
 276
 277 -- * Class 'Repeatable'
 278 class Repeatable repr where
 279   many0 :: repr a -> repr [a]
 280   many1 :: repr a -> repr [a]
 281   many0 = liftDerived1 many0
 282   many1 = liftDerived1 many1
 283   default many0 ::
 284     FromDerived1 Repeatable repr =>
 285     repr a -> repr [a]
 286   default many1 ::
 287     FromDerived1 Repeatable repr =>
 288     repr a -> repr [a]
 289
 290 -- * Class 'Permutable'
 291 class Permutable repr where
 292   -- Use @TypeFamilyDependencies@ to help type-inference infer @(repr)@.
 293   type Permutation (repr:: ReprKind) = (r :: ReprKind) | r -> repr
 294   type Permutation repr = Permutation (Derived repr)
 295   permutable :: Permutation repr a -> repr a
 296   perm :: repr a -> Permutation repr a
 297   noPerm :: Permutation repr ()
 298   permWithDefault :: a -> repr a -> Permutation repr a
 299   optionalPerm ::
 300     Eitherable repr => IsoFunctor repr => Permutable repr =>
 301     repr a -> Permutation repr (Maybe a)
 302   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 303
 304 (<&>) ::
 305   Permutable repr =>
 306   ProductFunctor (Permutation repr) =>
 307   repr a ->
 308   Permutation repr b ->
 309   Permutation repr (a, b)
 310 x <&> y = perm x <.> y
 311 infixr 4 <&>
 312 {-# INLINE (<&>)  #-}
 313
 314 (<?&>) ::
 315   Eitherable repr =>
 316   IsoFunctor repr =>
 317   Permutable repr =>
 318   ProductFunctor (Permutation repr) =>
 319   repr a ->
 320   Permutation repr b ->
 321   Permutation repr (Maybe a, b)
 322 x <?&> y = optionalPerm x <.> y
 323 infixr 4 <?&>
 324 {-# INLINE (<?&>) #-}
 325
 326 (<*&>) ::
 327   Eitherable repr =>
 328   Repeatable repr =>
 329   IsoFunctor repr =>
 330   Permutable repr =>
 331   ProductFunctor (Permutation repr) =>
 332   repr a ->
 333   Permutation repr b ->
 334   Permutation repr ([a],b)
 335 x <*&> y = permWithDefault [] (many1 x) <.> y
 336 infixr 4 <*&>
 337 {-# INLINE (<*&>) #-}
 338
 339 (<+&>) ::
 340   Eitherable repr =>
 341   Repeatable repr =>
 342   IsoFunctor repr =>
 343   Permutable repr =>
 344   ProductFunctor (Permutation repr) =>
 345   repr a ->
 346   Permutation repr b ->
 347   Permutation repr ([a], b)
 348 x <+&> y = perm (many1 x) <.> y
 349 infixr 4 <+&>
 350 {-# INLINE (<+&>) #-}
 351
 352 -- * Class 'Routable'
 353 class Routable repr where
 354   (<!>) :: repr a -> repr b -> repr (a, b); infixr 4 <!>
 355   (<!>) = liftDerived2 (<!>)
 356   default (<!>) ::
 357     FromDerived2 Routable repr =>
 358     repr a -> repr b -> repr (a, b)
 359
 360 -- | Like @(,)@ but @infixr@.
 361 -- Mostly useful for clarity when using 'Routable'.
 362 pattern (:!:) :: a -> b -> (a, b)
 363 pattern a:!:b <- (a, b)
 364   where a:!:b = (a, b)
 365 infixr 4 :!:
 366
 367 -- * Class 'Voidable'
 368 -- | FIXME: this class should likely be removed
 369 class Voidable repr where
 370   void :: a -> repr a -> repr ()
 371   void = liftDerived1 Fun.. void
 372   default void ::
 373     FromDerived1 Voidable repr =>
 374     a -> repr a -> repr ()
 375
 376 -- * Class 'Substractable'
 377 class Substractable repr where
 378   (<->) :: repr a -> repr b -> repr a; infixr 3 <->
 379   (<->) = liftDerived2 (<->)
 380   default (<->) ::
 381     FromDerived2 Substractable repr =>
 382     repr a -> repr b -> repr a