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