iface: rename syntax `Functionable` to `Unabstractable`

diff --git a/src/Symantic/Semantics/Data.hs b/src/Symantic/Semantics/Data.hs
index 5266a4ef606a920159695df257c9f06c46d871a6..11184702eb68198cb47be62d2890d83388c26a7e 100644 (file)
--- a/src/Symantic/Semantics/Data.hs
+++ b/src/Symantic/Semantics/Data.hs
@@ -137,19 +137,20 @@ instance Instantiable sem => Derivable (Data Instantiable sem) where
 instance Instantiable sem => Instantiable (SomeData sem) where
   f .@ x = SomeData (f :@ x)
 
--- Functionable
+-- Unabstractable
 instance
   ( Abstractable sem
   , Instantiable sem
   , Varable sem
   ) =>
-  Functionable (SomeData sem)
+  Unabstractable (SomeData sem)
   where
-  ($) = lam (\f -> lam (\x -> f .@ x))
-  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
+  ap = lam (\abc -> lam (\ab -> lam (\a -> abc .@ a .@ (ab .@ a))))
   const = lam (\x -> lam (\_y -> x))
-  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
   id = lam (\x -> x)
+  (.) = lam (\f -> lam (\g -> lam (\x -> f .@ (g .@ x))))
+  flip = lam (\f -> lam (\x -> lam (\y -> f .@ y .@ x)))
+  ($) = lam (\f -> lam (\x -> f .@ x))
 
 -- Anythingable
 data instance Data Anythingable sem a where

diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs
index 30df501132ca905acfa6ee4d2fb5742808eb91a3..c959c5f341815ace63559fe69d492f7d9c3f1237 100644 (file)
--- a/src/Symantic/Semantics/Forall.hs
+++ b/src/Symantic/Semantics/Forall.hs
@@ -16,11 +16,11 @@ import Control.Applicative (Applicative (..))
 import Control.Monad (Monad (..))
 import Data.Bool (Bool (..))
 import Data.Eq (Eq (..))
-import Data.Function ((.))
 import Data.Functor (Functor (..))
 import Data.Kind (Type)
 import Text.Show (Show (..))
 import Unsafe.Coerce (unsafeCoerce)
+import qualified Data.Function as Fun
 
 import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..))
 
@@ -30,17 +30,13 @@ newtype Forall (syns :: [Syntax]) (a :: Type)
 
 instance
   ( forall sem. Syntaxes syns sem => Functor sem
-  ) =>
-  Functor (Forall syns)
-  where
+  ) => Functor (Forall syns) where
   fmap f (Forall sem) = Forall (fmap f sem)
   a <$ (Forall sem) = Forall (a <$ sem)
 instance
   ( forall sem. Syntaxes syns sem => Applicative sem
   , Functor (Forall syns)
-  ) =>
-  Applicative (Forall syns)
-  where
+  ) => Applicative (Forall syns) where
   pure a = Forall (pure a)
   liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
   (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
@@ -49,9 +45,7 @@ instance
 instance
   ( forall sem. Syntaxes syns sem => Monad sem
   , Applicative (Forall syns)
-  ) =>
-  Monad (Forall syns)
-  where
+  ) => Monad (Forall syns) where
   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
   return = pure
   (>>) = (*>)
@@ -69,6 +63,15 @@ instance
       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
       forallSem :: sem a -> Forall syns a
       forallSem a = Forall (unsafeCoerce a)
+instance
+  ( forall sem. Syntaxes syns sem => Unabstractable sem
+  ) => Unabstractable (Forall syns) where
+  ap = Forall ap
+  const = Forall const
+  id = Forall id
+  (.) = Forall (.)
+  flip = Forall flip
+  ($) = Forall ($)
 
 -- * Type 'PerSyntax'
 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
@@ -105,4 +108,4 @@ class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
   perSyntax = PerSyntaxZ
 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
-  perSyntax = PerSyntaxS . perSyntax
+  perSyntax = PerSyntaxS Fun.. perSyntax

diff --git a/src/Symantic/Semantics/Viewer.hs b/src/Symantic/Semantics/Viewer.hs
index 48450a42b3c14d2e7d299ab1493513f3b3e02a39..5fb6d6bc5f18506c0582ce6aea5f74114f0546e0 100644 (file)
--- a/src/Symantic/Semantics/Viewer.hs
+++ b/src/Symantic/Semantics/Viewer.hs
@@ -102,6 +102,13 @@ instance Instantiable Viewer where
         Fun.. showString " "
         Fun.. showString name
   f .@ x = ViewerApp f x
+instance Unabstractable Viewer where
+  ap = ViewerInfix (infixL 4) "(<*>)" "<*>"
+  const = "const"
+  id = "id"
+  (.) = ViewerInfix (infixR 9) "(.)" "."
+  flip = flip
+  ($) = ViewerInfix (infixR 0) "($)" "$"
 instance Varable Viewer where
   var = Fun.id
 instance Anythingable Viewer

diff --git a/src/Symantic/Syntaxes/Classes.hs b/src/Symantic/Syntaxes/Classes.hs
index 88d2f027f46dca1e2e74c5165f56373cbe1147d0..f72b6de5e7fdc9c59f573bb910606a8fc460f623 100644 (file)
--- a/src/Symantic/Syntaxes/Classes.hs
+++ b/src/Symantic/Syntaxes/Classes.hs
@@ -93,34 +93,50 @@ class Instantiable sem where
     sem a ->
     sem b
 
--- ** Class 'Functionable'
-class Functionable sem where
+-- ** Class 'Unabstractable'
+-- | All operations in lambda calculus can be encoded
+-- via abstraction elimination into the SK calculus
+-- as binary trees whose leaves are one
+-- of the three symbols S ('ap') and K ('const').
+class Unabstractable sem where
+  -- | S
+  ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
+  -- | K
   const :: sem (a -> b -> a)
-  flip :: sem ((a -> b -> c) -> b -> a -> c)
+  -- | I
   id :: sem (a -> a)
+  -- | B
   (.) :: sem ((b -> c) -> (a -> b) -> a -> c)
   infixr 9 .
+  -- | C
+  flip :: sem ((a -> b -> c) -> b -> a -> c)
   ($) :: sem ((a -> b) -> a -> b)
   infixr 0 $
+
+  ap = liftDerived ap
   const = liftDerived const
-  flip = liftDerived flip
   id = liftDerived id
   (.) = liftDerived (.)
+  flip = liftDerived flip
   ($) = liftDerived ($)
+
+  default ap ::
+    FromDerived Unabstractable sem =>
+    sem ((a -> b -> c) -> (a -> b) -> a -> c)
   default const ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem (a -> b -> a)
-  default flip ::
-    FromDerived Functionable sem =>
-    sem ((a -> b -> c) -> b -> a -> c)
   default id ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem (a -> a)
   default (.) ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem ((b -> c) -> (a -> b) -> a -> c)
+  default flip ::
+    FromDerived Unabstractable sem =>
+    sem ((a -> b -> c) -> b -> a -> c)
   default ($) ::
-    FromDerived Functionable sem =>
+    FromDerived Unabstractable sem =>
     sem ((a -> b) -> a -> b)
 
 -- * Class 'Anythingable'