init

diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs
index c2f987f6fd745cd02a6e0875ff21051fbec10ce3..5514254390be41a71224f29d4db1eb642307aed9 100644 (file)
--- a/src/Symantic/Syntaxes.hs
+++ b/src/Symantic/Syntaxes.hs
@@ -2,36 +2,24 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+{-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
 
 module Symantic.Syntaxes where
 
-import Control.Applicative (Applicative (..))
-import Control.Monad (Monad (..))
-import Control.Monad.Trans.Except qualified as MT
-import Control.Monad.Trans.Reader qualified as MT
-import Control.Monad.Trans.State qualified as MT
-import Data.Bool (otherwise)
 import Data.Either (Either (..))
-import Data.Eq (Eq (..))
-import Data.Function (id, ($), (.))
-import Data.Functor (Functor (..), (<$>))
-import Data.Functor.Constant (Constant (..))
+import Data.Function (($))
 import Data.Int (Int)
-import Data.Kind (Constraint, Type)
-import Data.Maybe (Maybe (..), isJust)
-import Data.Proxy (Proxy (..))
+import Data.Kind (Type)
+import Data.Maybe (Maybe (..))
 import Data.Semigroup (Semigroup (..))
-import Data.String (String)
-import GHC.Types
-import Text.Read (Read (..), reads)
 import Text.Show (Show (..))
-import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, (:~~:) (..))
+import Type.Reflection (typeRep, (:~~:) (..))
 import Unsafe.Coerce (unsafeCoerce)
 import Prelude (error)
-import Prelude qualified
 
 import Symantic
-import Symantic.Typer
+import Symantic.Typer ()
 
 class Addable sem where
   lit :: Int -> sem Int
@@ -41,7 +29,7 @@ class Mulable sem where
   mul :: sem Int -> sem Int -> sem Int
 class Abstractable sem where
   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
-  lam :: Typeable a => (sem a -> sem b) -> sem (a -> b)
+  lam :: Tyable a => (sem a -> sem b) -> sem (a -> b)
 
   -- | Application, aka. unabstract.
   (.@) :: sem (a -> b) -> sem a -> sem b
@@ -62,7 +50,7 @@ instance
   ForallSem a2b .@ ForallSem a = ForallSem (a2b .@ a)
   lam f = ForallSem (lam (\a -> let ForallSem b = f (forallSem a) in b))
     where
-      -- Safe here because a :: sem a and b :: sem b share the same 'sem'.
+      -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
       forallSem :: sem a -> ForallSem syn a
       forallSem a = ForallSem (unsafeCoerce a)
 
@@ -183,7 +171,7 @@ instance Abstractable Printer where
       BinTree0
         ( TokenTermAbst
             "x"
-            (TyVT TyConst{tyConst = Const{constType = typeRep @a, constMeta = ()}, tyConstLen = LenZ})
+            (TyVT (typeOf @a))
             (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x")))))
         )
 
@@ -205,7 +193,7 @@ parse = fix parseAbstractable
 
 tree0 = add (lit 8) (neg (add (lit 1) (lit 2)))
 tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
-tree2 = lam (\(x :: sem Int) -> mul (lit 0) (add (lit 1) (lit 2)))
+tree2 = lam (\(x :: sem Int) -> mul (lit 0) (add (lit 1) x))
 tree0Print = print tree0
 tree1Print = print tree1
 tree2Print = print tree2

diff --git a/src/Symantic/Typer/Type.hs b/src/Symantic/Typer/Type.hs
index 68e2754c032d3537b1eb4f7d75ea2238864a34c3..36da34b51b368bbf9261b09646d1db0203307438 100644 (file)
--- a/src/Symantic/Typer/Type.hs
+++ b/src/Symantic/Typer/Type.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-partial-fields #-}
@@ -206,6 +207,14 @@ data Ty :: forall aK. Type -> [Type] -> aK -> Type where
   TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a)
 infixl 9 `TyApp`
 
+-- ** Class 'Tyable'
+class Tyable a where
+  typeOf :: Monoid meta => Ty meta '[] a
+instance (Tyable a, Tyable b) => Tyable (a b) where
+  typeOf = TyApp (typeOf @a) (typeOf @b)
+instance {-# OVERLAPPABLE #-} Typeable a => Tyable a where
+  typeOf = TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = LenZ}
+
 pattern FUN ::
   -- CReq
   forall k (fun :: k) meta vs.