From f33e08d27702bae9339fe99905e44e6607192e27 Mon Sep 17 00:00:00 2001 From: Julien Moutinho <julm@sourcephile.fr> Date: Sat, 5 Aug 2023 13:48:46 +0200 Subject: [PATCH] init --- .gitignore | 21 ++ .reuse/dep5 | 10 +- flake.nix | 2 +- src/ForallSem.hs | 547 ---------------------------------- src/Symantic/Compiler.hs | 5 + src/Symantic/Compiler/Term.hs | 72 +++++ src/Symantic/Parser.hs | 83 ++++++ src/Symantic/Parser/Error.hs | 23 ++ src/Symantic/Parser/Source.hs | 89 ++++++ src/Symantic/Printer.hs | 34 +++ src/Symantic/Syntaxes.hs | 226 ++++++++++++++ src/Symantic/Typer.hs | 11 + src/Symantic/Typer/Eq.hs | 14 + src/Symantic/Typer/List.hs | 47 +++ src/Symantic/Typer/Type.hs | 467 +++++++++++++++++++++++++++++ src/Symantic/Typer/Unify.hs | 269 +++++++++++++++++ symantic.cabal | 206 ++----------- 17 files changed, 1396 insertions(+), 730 deletions(-) create mode 100644 .gitignore delete mode 100644 src/ForallSem.hs create mode 100644 src/Symantic/Compiler.hs create mode 100644 src/Symantic/Compiler/Term.hs create mode 100644 src/Symantic/Parser.hs create mode 100644 src/Symantic/Parser/Error.hs create mode 100644 src/Symantic/Parser/Source.hs create mode 100644 src/Symantic/Printer.hs create mode 100644 src/Symantic/Syntaxes.hs create mode 100644 src/Symantic/Typer.hs create mode 100644 src/Symantic/Typer/Eq.hs create mode 100644 src/Symantic/Typer/List.hs create mode 100644 src/Symantic/Typer/Type.hs create mode 100644 src/Symantic/Typer/Unify.hs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2f00fe6 --- /dev/null +++ b/.gitignore @@ -0,0 +1,21 @@ +*.actual.* +*.eventlog +*.eventlog.html +*.eventlog.json +*.hi +*.hp +*.o +*.orig +*.prof +*.root +*~ +.direnv/ +.ghc.environment.* +.shake +.stack-work/ +/.direnv +/.pre-commit-config.yaml +dist-newstyle/ +dump-core/ +hlint.html +result* diff --git a/.reuse/dep5 b/.reuse/dep5 index 4db55a9..e110498 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -1,13 +1,13 @@ Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ -Upstream-Name: literate-web -Upstream-Contact: Julien Moutinho <julm+literate-web@sourcephile.fr> -Source: https://git.sourcephile.fr/haskell/literate-web +Upstream-Name: symantic +Upstream-Contact: Julien Moutinho <julm+symantic@sourcephile.fr> +Source: https://git.sourcephile.fr/haskell/symantic Files: *.lock cabal.project* *.cabal *.md .chglog/* .envrc .gitignore .gitmodules .git-blame-ignore-revs *.yaml -Copyright: Julien Moutinho <julm+literate-web@sourcephile.fr> +Copyright: Julien Moutinho <julm+symantic@sourcephile.fr> License: CC0-1.0 Files: src/* tests/* Makefile *.nix -Copyright: Julien Moutinho <julm+literate-web@sourcephile.fr> +Copyright: Julien Moutinho <julm+symantic@sourcephile.fr> License: AGPL-3.0-or-later diff --git a/flake.nix b/flake.nix index 6fbe0ea..da7bddd 100644 --- a/flake.nix +++ b/flake.nix @@ -13,7 +13,7 @@ forAllSystems = f: lib.genAttrs lib.systems.flakeExposed (system: f rec { inherit system; pkgs = inputs.nixpkgs.legacyPackages.${system}; - haskellPackages = pkgs.haskellPackages.extend (with pkgs.haskell.lib; hfinal: hsuper: { + haskellPackages = pkgs.haskell.packages.ghc92.extend (with pkgs.haskell.lib; hfinal: hsuper: { ${pkg} = doBenchmark (buildFromSdist (hfinal.callCabal2nix pkg ./. { })); symantic-base = buildFromSdist (hfinal.callCabal2nix "symantic-base" inputs.symantic-base { }); }); diff --git a/src/ForallSem.hs b/src/ForallSem.hs deleted file mode 100644 index 342f22b..0000000 --- a/src/ForallSem.hs +++ /dev/null @@ -1,547 +0,0 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE NoMonomorphismRestriction #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE UndecidableSuperClasses #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ViewPatterns #-} - -module ForallSem where - -import Data.Functor (Functor(..), (<$>)) -import Data.Functor.Constant (Constant(..)) -import Control.Applicative (Applicative(..)) -import Control.Monad (Monad(..)) -import Data.Kind (Type, Constraint) -import Data.Function (($), (.), id) -import Data.String (String) -import Data.Semigroup (Semigroup(..)) -import Data.Maybe (Maybe(..), isJust) -import Text.Read (Read(..), reads) -import Data.Bool (otherwise) -import Text.Show (Show(..)) -import Data.Eq (Eq(..)) -import Data.Either (Either(..)) -import Data.Int (Int) -import Prelude (error) -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 Type.Reflection -import Unsafe.Coerce (unsafeCoerce) -import Data.Proxy (Proxy(..)) -import Prelude qualified -import GHC.Types - -type Semantic = Type -> Type -type Syntax = Semantic -> Constraint -class Syn0 (sem::Semantic) where - syn0 :: sem () -class Syn1 (sem::Semantic) where - syn1 :: sem () -class Syn2 (sem::Semantic) where - syn2 :: sem () -> sem () -> sem () - -p0 :: (forall sem. syn sem => Syn0 sem) => ForallSem syn () -p0 = ForallSem syn0 - -p1 :: (forall sem. syn sem => Syn1 sem) => ForallSem syn () -p1 = ForallSem syn1 - -p3 :: forall syn. - ( forall sem. syn sem => Syn0 sem - , forall sem. syn sem => Syn1 sem - , forall sem. syn sem => Syn2 sem - ) => ForallSem syn () -p3 = ForallSem $ syn2 (unForallSem @syn p0) (unForallSem @syn p1) - - - - - - - -data ForallSem (syn::Syntax) (a::Type) - = ForallSem { unForallSem :: forall sem. syn sem => sem a } - -instance ( forall sem. syn sem => Functor sem - ) => Functor (ForallSem syn) where - fmap f (ForallSem sem) = ForallSem (fmap f sem) - a <$ (ForallSem sem) = ForallSem (a <$ sem) -instance ( forall sem. syn sem => Applicative sem - , Functor (ForallSem syn) - ) => Applicative (ForallSem syn) where - pure a = ForallSem (pure a) - liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b) - (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a) - (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a) - (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a) -instance ( forall sem. syn sem => Monad sem - , Applicative (ForallSem syn) - ) => Monad (ForallSem syn) where - (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb) - return = pure - (>>) = (*>) - --- * Interpreter 'Parser' -data TermVT syn = forall vs a. TermVT - { typeTermVT :: Ty vs a - , unTermVT :: ForallSem syn a - } - --- instance Eq (TyVT) where --- TyVT x == TyVT y = --- let (x', y') = appendVars x y in --- isJust $ eqTypeKi x' y' - --- * Type family @(++)@ -type family (++) xs ys where - '[] ++ ys = ys - -- xs ++ '[] = xs - (x ': xs) ++ ys = x ': xs ++ ys -infixr 5 ++ - --- * Type 'Len' -data Len (xs::[k]) where - LenZ :: Len '[] - LenS :: Len xs -> Len (x ': xs) - -instance Show (Len vs) where - showsPrec _p = showsPrec 10 . intLen - -addLen :: Len a -> Len b -> Len (a ++ b) -addLen LenZ b = b -addLen (LenS a) b = LenS $ addLen a b - -shiftLen :: forall t b a. Len a -> Len (a ++ b) -> Len (a ++ t ': b) -shiftLen LenZ b = LenS b -shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b - -intLen :: Len xs -> Int -intLen = go 0 - where - go :: Int -> Len xs -> Int - go i LenZ = i - go i (LenS l) = go (1 Prelude.+ i) l - --- ** Class 'LenInj' -class LenInj (vs::[k]) where - lenInj :: Len vs -instance LenInj '[] where - lenInj = LenZ -instance LenInj as => LenInj (a ': as) where - lenInj = LenS lenInj - -type Name = String --- Use a CUSK, because it's a polymorphically recursive type, --- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/ -data Ty :: forall aK. [Type] -> aK -> Type where - TyConst :: Len vs -> TypeRep a -> Ty vs a - TyVar :: Name -> Var vs a -> Ty vs a - TyApp :: Ty vs f -> Ty vs a -> Ty vs (f a) -infixl 9 `TyApp` -deriving instance Show (Ty vs a) -instance AllocVars Ty where - allocVarsL len (TyConst l c) = TyConst (addLen len l) c - allocVarsL len (TyApp f a) = TyApp (allocVarsL len f) (allocVarsL len a) - allocVarsL len (TyVar n v) = TyVar n (allocVarsL len v) - --allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as - - allocVarsR len (TyConst l c) = TyConst (addLen l len) c - allocVarsR len (TyApp f a) = TyApp (allocVarsR len f) (allocVarsR len a) - allocVarsR len (TyVar n v) = TyVar n (allocVarsR len v) - --allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as - -data TyVT = forall vs a. TyVT (Ty vs a) -deriving instance Show TyVT -instance Eq TyVT where - TyVT x == TyVT y = isJust (eqTyKi x' y') - where (x', y') = appendVars x y - --- | /Heterogeneous type equality/: --- return two proofs when two 'Type's are equals: --- one for the type and one for the kind. -eqTyKi :: Ty vs (x::xK) -> Ty vs (y::yK) -> Maybe (x:~~:y) -eqTyKi (TyConst _lx x) (TyConst _ly y) = eqTypeRep x y -eqTyKi (TyVar _nx x) (TyVar _ny y) = eqVarKi x y -eqTyKi (TyApp fx ax) (TyApp fy ay) - | Just HRefl <- eqTyKi fx fy - , Just HRefl <- eqTyKi ax ay - = Just HRefl --- eqTyKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) --- | Just HRefl <- eqTypeRep fx fy --- , Just HRefl <- eqTypes ax ay --- = Just HRefl --- -- NOTE: 'TyFam' is expanded as much as possible. --- eqTyKi x@TyFam{} y = eqTyKi (expandFam x) y --- eqTyKi x y@TyFam{} = eqTyKi x (expandFam y) -eqTyKi _x _y = Nothing - --- data Some :: (Type -> Type) -> Type where --- Some :: TypeRep a -> t a -> Some t --- --- mapSome :: (forall a. s a -> t a) -> Some s -> Some t --- mapSome f (Some a t) = Some a (f t) --- --- type SomeTy = Some (Constant ()) - --- pattern SomeTy :: TypeRep a -> SomeTy --- pattern SomeTy a = Some a (Constant ()) --- {-# COMPLETE SomeTy #-} - --- someType :: TypeRep a -> SomeTy --- someType a = Some a (Constant ()) - ---infer :: Vars vs -> TermVT syn -> Maybe (TermVT syn) ---infer ctx te = case te of ---Lit i -> return $ Some TTyInt (embed (CInt i)) - - -data Parser syn = Parser - { unParser :: - --MT.State (TokenTerm a) - (Either ErrMsg (TermVT syn)) - } - -{- -instance ( forall sem. syn sem => Functor sem - ) => Functor (Parser syn) where - fmap f (Parser esa) = Parser $ - case esa of - Left e -> Left e - Right (ForallSem sem) -> Right (ForallSem (f <$> sem)) - a <$ Parser esa = Parser $ - case esa of - Left e -> Left e - Right (ForallSem sem) -> Right (ForallSem (a <$ sem)) -instance ( forall sem. syn sem => Applicative sem - , Applicative (ForallSem syn) - , forall err. syn (Either err) - , syn (Parser syn) -- FIXME: what constraint is still missing to still require that? - ) => Applicative (Parser syn) where - pure a = Parser (Right (ForallSem (pure a))) - liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b) - (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a) - (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a) - (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a) -instance ( forall sem. syn sem => Monad sem - , forall err. syn (Either err) - , syn (Parser syn) -- FIXME: what constraint is still missing to still require that? - ) => Monad (Parser syn) where - (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f) --} - --- * Type 'BinTree' --- | /Binary Tree/. -data BinTree a - = BinTree0 a - | BinTree2 (BinTree a) (BinTree a) - deriving (Eq, Show) - -type TermAST = BinTree TokenTerm -data TokenTerm - = TokenTermAtom String - | TokenTermAbst String TyVT TermAST - deriving (Show) - -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))) -tree0Print = print tree0 -tree1Print = print tree1 -tree2Print = print tree2 - -type ErrMsg = String - -safeRead :: Read a => String -> Either ErrMsg a -safeRead s = case reads s of - [(x,"")] -> Right x - _ -> Left $ "Read error: " <> s - -instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where - lit n = ForallSem (lit n) - neg (ForallSem a) = ForallSem (neg a) - add (ForallSem a) (ForallSem b) = ForallSem (add a b) -instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where - mul (ForallSem a) (ForallSem b) = ForallSem (mul a b) -instance ( forall sem. syn sem => Abstractable sem - --, forall sem. syn sem => Typeable sem -- user instance not accepted - --, forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy... - ) => Abstractable (ForallSem syn) where - 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'. - forallSem :: sem a -> ForallSem syn a - forallSem a = ForallSem (unsafeCoerce a) - - - -parseAddable :: - ( forall sem. syn sem => Addable sem - , syn (ForallSem syn) - ) => - (TermAST -> Parser syn) -> TermAST -> Parser syn -parseAddable _final (BinTree0 (TokenTermAtom s)) - | Right (i::Int) <- safeRead s - = Parser $ Right $ TermVT (TyConst LenZ typeRep) $ ForallSem @_ @Int $ lit i -parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $ - case final aT of - Parser aE -> do - TermVT aTy (ForallSem a :: ForallSem syn a) <- aE - case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of - Nothing -> Left "TypeError" - Just HRefl -> do - Right $ TermVT aTy $ neg a -parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) = - Parser $ do - TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT) - case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of - Nothing -> Left "TypeError" - Just HRefl -> do - TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT) - case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of - Nothing -> Left "TypeError" - Just HRefl -> do - Right $ TermVT aTy $ ForallSem @_ @Int $ add a b -parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e - ---tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int) ---tree0Parser = unParser $ parse tree0Print - -class (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem -instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem - -parseMulable :: - ( forall sem. syn sem => Mulable sem - , forall sem. syn sem => Addable sem - , syn (ForallSem syn) - ) => - (TermAST -> Parser syn) -> TermAST -> Parser syn -parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) = - Parser $ do - case (final aT, final bT) of - (Parser aE, Parser bE) -> do - TermVT aTy (ForallSem a :: ForallSem syn a) <- aE - case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of - Nothing -> Left "TypeError" - Just HRefl -> do - TermVT bTy (ForallSem b :: ForallSem syn b) <- bE - case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of - Nothing -> Left "TypeError" - Just HRefl -> do - Right $ TermVT aTy (ForallSem @_ @a $ mul a b) -parseMulable final t = parseAddable final t - -parseAbstractable :: - ( forall sem. syn sem => Mulable sem - , forall sem. syn sem => Addable sem - , forall sem. syn sem => Abstractable sem - , syn (ForallSem syn) - ) => - a ~ Int => - (TermAST -> Parser syn) -> TermAST -> Parser syn --- TODO: parse variables -parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy::Ty vs a)) bT)) = - Parser $ - case final bT of - Parser bE -> do - TermVT abTy (abF :: ForallSem syn ab) <- bE - case eqTyKi (TyConst (lenVars aTy) (typeRep @Type)) aTy of - Nothing -> Left "TypeError" - Just HRefl -> do - case abTy of - FUN iTy bTy -> - case eqTyKi (TyConst (lenVars bTy) (typeRep @Type)) bTy of - Nothing -> Left "TypeError" - Just HRefl -> do - -- FIXME: appendVars - case eqTyKi aTy iTy of - Nothing -> Left "TypeError" - Just HRefl -> do - case abF of - ForallSem ab -> - Right $ TermVT abTy $ ForallSem @_ @ab $ - -- FIXME: Tyable - lam (ab .@) - _ -> Left "TypeError" -parseAbstractable final t = parseMulable final t - -pattern FUN :: forall k (fun :: k) vs. () - => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) - (arg :: TYPE r1) (res :: TYPE r2). - (k ~ Type, fun ~~ (arg -> res)) - => Ty vs arg - -> Ty vs res - -> Ty vs fun -pattern FUN arg res <- (TyConst _len (eqTypeRep (typeRep @(->)) -> Just HRefl) `TyApp` arg) `TyApp` res - where FUN arg res = (TyConst (lenVars arg) (typeRep @(->)) `TyApp` arg) `TyApp` res - --- * Class 'LenVars' --- | Return the 'Len' of the 'Var' context. -class LenVars a where - lenVars :: a -> Len (VarsOf a) - -type instance VarsOf (Ty vs a) = vs -instance LenVars (Ty vs a) where - lenVars (TyConst len _c) = len - lenVars (TyApp f _a) = lenVars f - lenVars (TyVar _n v) = lenVars v - -- lenVars (TyFam l _f _as) = l - --- * Type family 'VarsOf' --- | Return the 'Var' context of something. -type family VarsOf a :: [Type] -type instance VarsOf (Var vs v) = vs ---type instance VarsOf (UsedVars src vs vs') = vs' - - - --- * Class 'AllocVars' --- | Allocate 'Var's in a 'Var' context, --- either to the left or to the right. -class AllocVars (a::[Type] -> k -> Type) where - allocVarsL :: Len len -> a vs x -> a (len ++ vs) x - allocVarsR :: Len len -> a vs x -> a (vs ++ len) x - -appendVars :: - AllocVars a => - AllocVars b => - LenVars (a vs_x x) => - LenVars (b vs_y y) => - VarsOf (a vs_x x) ~ vs_x => - VarsOf (b vs_y y) ~ vs_y => - a vs_x (x::kx) -> - b vs_y (y::ky) -> - ( a (vs_x ++ vs_y) x - , b (vs_x ++ vs_y) y ) -appendVars x y = - ( allocVarsR (lenVars y) x - , allocVarsL (lenVars x) y - ) - - - --- Var -data Var (vs::[Type]) (v::vK) :: Type where - VarZ :: TypeRep vk -> Len (Proxy (v::vK) ': vs) -> Var (Proxy (v::vK) ': vs) v - VarS :: Var vs v -> Var (not_v ': vs) v -instance AllocVars Var where - allocVarsL LenZ v = v - allocVarsL (LenS len) v = VarS (allocVarsL len v) - - allocVarsR len (VarZ k l) = VarZ k (addLen l len) - allocVarsR len (VarS v) = VarS (allocVarsR len v) - -data VarV vs = forall v. VarV (Var vs v) -instance LenVars (Var vs v) where - lenVars (VarZ _k l) = l - lenVars (VarS v) = LenS (lenVars v) - -deriving instance Show (Var vs v) - -eqVarKi :: Var vs x -> Var vs y -> Maybe ((x::kx) :~~: (y::ky)) -eqVarKi VarZ{} VarZ{} = Just HRefl -eqVarKi (VarS x) (VarS y) = eqVarKi x y -eqVarKi _ _ = Nothing - --- Vars -data Vars (vs::[Type]) :: Type where - -- VarsZ represents an empty context. - VarsZ :: Vars '[] - -- A cons stores a variable name and its type, - -- and then the rest of the context. - VarsS :: String -> TypeRep vK -> Vars vs -> Vars (Proxy (v::vK) ': vs) -type instance VarsOf (Vars vs) = vs -instance LenVars (Vars vs) where - lenVars VarsZ = LenZ - lenVars (VarsS _n _kv vs) = LenS $ lenVars vs - - --- Vars -data Env :: [Type] -> Type where - ENil :: Env '[] - ECons :: v -> Env vs -> Env (v ': vs) - --- (!) :: Env vs -> Var vs v -> v --- (ECons x _) ! VarZ = x --- (ECons _ e) ! (VarS x) = e ! x --- ENil ! _ = error "GHC can't tell this is impossible" - -lookupVars :: String -> Vars vs -> Maybe (VarV vs) -lookupVars _ VarsZ = Nothing -lookupVars n (VarsS vN vK vs) - | n == vN = Just (VarV (VarZ vK (LenS (lenVars vs)))) - | otherwise = (\(VarV v) -> VarV (VarS v)) <$> lookupVars n vs - - -fix :: (a -> a) -> a -fix f = f (fix f) - -parse :: - ( forall sem. syn sem => Addable sem - , forall sem. syn sem => Mulable sem - , forall sem. syn sem => Abstractable sem - , syn (ForallSem syn) - ) => - TermAST -> Parser syn -parse = fix parseAbstractable - -tree0ParsePrint :: TermAST -tree0ParsePrint = case parse @FinalSyntaxes tree0Print of - Parser (Left e) -> error e - Parser (Right (TermVT _ty (ForallSem sem))) -> print sem - -tree1ParsePrint :: TermAST -tree1ParsePrint = case parse @FinalSyntaxes tree1Print of - Parser (Left e) -> error e - Parser (Right (TermVT _ty (ForallSem sem))) -> print sem - -tree2ParsePrint :: TermAST -tree2ParsePrint = case parse @FinalSyntaxes tree2Print of - Parser (Left e) -> error e - Parser (Right (TermVT _ty (ForallSem sem))) -> print sem - -class Addable sem where - lit :: Int -> sem Int - neg :: sem Int -> sem Int - add :: sem Int -> sem Int -> sem Int -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) - -- | Application, aka. unabstract. - (.@) :: sem (a -> b) -> sem a -> sem b - - --- * Interpreter 'Printer' -newtype Printer a = Printer { unPrinter :: TermAST } -print :: Printer a -> TermAST -print = unPrinter -print2 :: String -> Printer a1 -> Printer a2 -> Printer a3 -print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT -instance Addable Printer where - lit n = Printer $ BinTree0 (TokenTermAtom (show n)) - neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT - add = print2 "Add" -instance Mulable Printer where - mul = print2 "Mul" -instance Abstractable Printer where - Printer f .@ Printer a = Printer $ BinTree2 f a - lam (f::Printer a -> Printer b) = Printer $ - -- FIXME: Tyable? instead of Typeable? - BinTree0 (TokenTermAbst "x" (TyVT (TyConst (lenInj @_ @'[]) (typeRep @a))) - (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x")))))) diff --git a/src/Symantic/Compiler.hs b/src/Symantic/Compiler.hs new file mode 100644 index 0000000..2fea388 --- /dev/null +++ b/src/Symantic/Compiler.hs @@ -0,0 +1,5 @@ +module Symantic.Compiler ( + module Symantic.Compiler.Term, +) where + +import Symantic.Compiler.Term diff --git a/src/Symantic/Compiler/Term.hs b/src/Symantic/Compiler/Term.hs new file mode 100644 index 0000000..42307ea --- /dev/null +++ b/src/Symantic/Compiler/Term.hs @@ -0,0 +1,72 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +module Symantic.Compiler.Term 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.Int (Int) +import Data.Kind (Constraint, Type) +import Data.Maybe (Maybe (..), isJust) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (Semigroup (..)) +import Data.String (String) +import GHC.Types +import Text.Read (Read (..), reads) +import Text.Show (Show (..)) +import Unsafe.Coerce (unsafeCoerce) +import Prelude (error) +import Prelude qualified + +import Symantic.Typer + +type Semantic = Type -> Type +type Syntax = Semantic -> Constraint + +data ForallSem (syn :: Syntax) (a :: Type) = ForallSem {unForallSem :: forall sem. syn sem => sem a} + +instance + ( forall sem. syn sem => Functor sem + ) => + Functor (ForallSem syn) + where + fmap f (ForallSem sem) = ForallSem (fmap f sem) + a <$ (ForallSem sem) = ForallSem (a <$ sem) +instance + ( forall sem. syn sem => Applicative sem + , Functor (ForallSem syn) + ) => + Applicative (ForallSem syn) + where + pure a = ForallSem (pure a) + liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b) + (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a) + (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a) + (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a) +instance + ( forall sem. syn sem => Monad sem + , Applicative (ForallSem syn) + ) => + Monad (ForallSem syn) + where + (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb) + return = pure + (>>) = (*>) + +-- * Interpreter 'Parser' +data TermVT syn = forall vs a. + TermVT + { typeTermVT :: Ty () vs a + , unTermVT :: ForallSem syn a + } diff --git a/src/Symantic/Parser.hs b/src/Symantic/Parser.hs new file mode 100644 index 0000000..d031073 --- /dev/null +++ b/src/Symantic/Parser.hs @@ -0,0 +1,83 @@ +module Symantic.Parser 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.Int (Int) +import Data.Kind (Constraint, Type) +import Data.Maybe (Maybe (..), isJust) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (Semigroup (..)) +import Data.String (String) +import GHC.Types +import Text.Read (Read (..), reads) +import Text.Show (Show (..)) +import Unsafe.Coerce (unsafeCoerce) +import Prelude (error) +import Prelude qualified + +import Symantic.Compiler +import Symantic.Typer + +-- * Type 'Parser' +data Parser syn = Parser + { unParser :: + ( -- MT.State (TokenTerm a) + Either ErrMsg (TermVT syn) + ) + } +type ErrMsg = String +-- * Type 'BinTree' + +-- | /Binary Tree/. +data BinTree a + = BinTree0 a + | BinTree2 (BinTree a) (BinTree a) + deriving (Eq, Show) + +type TermAST = BinTree TokenTerm +data TokenTerm + = TokenTermAtom String + | TokenTermAbst String (TyVT ()) TermAST + deriving (Show) + +safeRead :: Read a => String -> Either ErrMsg a +safeRead s = case reads s of + [(x, "")] -> Right x + _ -> Left $ "Read error: " <> s + +{- +instance ( forall sem. syn sem => Functor sem + ) => Functor (Parser syn) where + fmap f (Parser esa) = Parser $ + case esa of + Left e -> Left e + Right (ForallSem sem) -> Right (ForallSem (f <$> sem)) + a <$ Parser esa = Parser $ + case esa of + Left e -> Left e + Right (ForallSem sem) -> Right (ForallSem (a <$ sem)) +instance ( forall sem. syn sem => Applicative sem + , Applicative (ForallSem syn) + , forall err. syn (Either err) + , syn (Parser syn) -- FIXME: what constraint is still missing to still require that? + ) => Applicative (Parser syn) where + pure a = Parser (Right (ForallSem (pure a))) + liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b) + (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a) + (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a) + (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a) +instance ( forall sem. syn sem => Monad sem + , forall err. syn (Either err) + , syn (Parser syn) -- FIXME: what constraint is still missing to still require that? + ) => Monad (Parser syn) where + (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f) +-} diff --git a/src/Symantic/Parser/Error.hs b/src/Symantic/Parser/Error.hs new file mode 100644 index 0000000..ed697bc --- /dev/null +++ b/src/Symantic/Parser/Error.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE TypeApplications #-} + +module Symantic.Parser.Error where + +import Data.Either (Either (..)) +import Data.Function (($), (.)) +import Data.Proxy (Proxy) + +-- * Class 'ErrorInj' +class ErrorInj a b where + errorInj :: a -> b +instance ErrorInj err e => ErrorInj err (Either e a) where + errorInj = Left . errorInj + +liftError :: + forall e0 err e1 a. + ErrorInj e0 e1 => + ErrorInj e1 err => + Proxy e1 -> + Either e0 a -> + Either err a +liftError _e1 (Right a) = Right a +liftError _e1 (Left e) = Left $ errorInj @e1 @err $ errorInj @e0 @e1 e diff --git a/src/Symantic/Parser/Source.hs b/src/Symantic/Parser/Source.hs new file mode 100644 index 0000000..a2c5e72 --- /dev/null +++ b/src/Symantic/Parser/Source.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +-- {-# LANGUAGE PolyKinds #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Symantic.Parser.Source where + +import Control.Applicative (Applicative (..)) +import Control.Monad (Monad (..)) +import Control.Monad.Classes qualified as MC +import Control.Monad.Trans.Writer.CPS qualified as MT +import Data.Bool (Bool (..)) +import Data.Eq (Eq) +import Data.Function ((.)) +import Data.Functor (Functor) +import Data.Functor.Classes (Show1 (..), liftShowList2, liftShowsPrec2, showsPrec1, showsUnaryWith) +import Data.Kind (Type) +import Data.Monoid (Monoid (..)) +import Data.Ord (Ord) +import Data.Semigroup (Semigroup (..)) +import Data.Tuple (fst) +import Data.Typeable (Typeable) +import Text.Show (Show (..)) + +-- * Class 'Source' +class Monoid src => Source src +instance Source () + +-- ** Class 'SourceInj' +class Source src => SourceInj a src where + sourceInj :: a -> src +instance SourceInj a () where + sourceInj _ = () + +-- ** Type family 'SourceOf' +type family SourceOf a + +-- ** Type 'Sourceable' +class Source (SourceOf a) => Sourceable a where + sourceOf :: a -> SourceOf a + setSource :: a -> SourceOf a -> a +infixl 5 `setSource` + +withSource :: SourceInj src (SourceOf a) => Sourceable a => a -> src -> a +withSource a src = a `setSource` sourceInj src + +-- ** Type 'Source_Input' +type family Source_Input (src :: Type) :: Type +type instance Source_Input () = () + +-- ** Type 'Span' +data Span src = Span + { spanBegin :: !src + , spanEnd :: !src + } + deriving (Eq, Ord, Show, Typeable) + +type Sourced src a = MT.Writer src a +unSourced :: Monoid src => Sourced src a -> a +unSourced = fst . MT.runWriter + +instance (Show w, Monoid w, Show1 m, Show a) => Show (MT.WriterT w m a) where + showsPrec = showsPrec1 + +instance (Show w, Monoid w, Show1 m) => Show1 (MT.WriterT w m) where + liftShowsPrec sp sl d m = + showsUnaryWith (liftShowsPrec sp' sl') "WriterT" d (MT.runWriterT m) + where + sp' = liftShowsPrec2 sp sl showsPrec showList + sl' = liftShowList2 sp sl showsPrec showList + +appendSource :: MC.MonadWriter src m => m a -> src -> m a +appendSource m src = do + a <- m + MC.tell src + return a + +-- class MC.MonadWriter w m => Provenanceable w (m::Type -> Type) +-- instance MC.MonadWriter w m => Provenanceable w m +-- type Provenanceable w m = MC.MonadWriter w m + +type instance MC.CanDo (MT.WriterT w m) eff = WriterCanDo w eff +type family WriterCanDo w eff where + WriterCanDo w (MC.EffWriter w) = 'True + WriterCanDo w eff = 'False + +class Provenanceable prov sem where + provenance :: prov -> sem prov diff --git a/src/Symantic/Printer.hs b/src/Symantic/Printer.hs new file mode 100644 index 0000000..484d9ea --- /dev/null +++ b/src/Symantic/Printer.hs @@ -0,0 +1,34 @@ +module Symantic.Printer 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.Int (Int) +import Data.Kind (Constraint, Type) +import Data.Maybe (Maybe (..), isJust) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (Semigroup (..)) +import Data.String (String) +import GHC.Types +import Text.Read (Read (..), reads) +import Text.Show (Show (..)) +import Unsafe.Coerce (unsafeCoerce) +import Prelude (error) +import Prelude qualified + +import Symantic.Compiler +import Symantic.Parser + +newtype Printer a = Printer {unPrinter :: TermAST} +print :: Printer a -> TermAST +print = unPrinter +print2 :: String -> Printer a1 -> Printer a2 -> Printer a3 +print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT diff --git a/src/Symantic/Syntaxes.hs b/src/Symantic/Syntaxes.hs new file mode 100644 index 0000000..c2f987f --- /dev/null +++ b/src/Symantic/Syntaxes.hs @@ -0,0 +1,226 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +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.Int (Int) +import Data.Kind (Constraint, Type) +import Data.Maybe (Maybe (..), isJust) +import Data.Proxy (Proxy (..)) +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 Unsafe.Coerce (unsafeCoerce) +import Prelude (error) +import Prelude qualified + +import Symantic +import Symantic.Typer + +class Addable sem where + lit :: Int -> sem Int + neg :: sem Int -> sem Int + add :: sem Int -> sem Int -> sem Int +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) + + -- | Application, aka. unabstract. + (.@) :: sem (a -> b) -> sem a -> sem b + +instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where + lit n = ForallSem (lit n) + neg (ForallSem a) = ForallSem (neg a) + add (ForallSem a) (ForallSem b) = ForallSem (add a b) +instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where + mul (ForallSem a) (ForallSem b) = ForallSem (mul a b) +instance + ( forall sem. syn sem => Abstractable sem + -- , forall sem. syn sem => Typeable sem -- user instance not accepted + -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy... + ) => + Abstractable (ForallSem syn) + where + 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'. + forallSem :: sem a -> ForallSem syn a + forallSem a = ForallSem (unsafeCoerce a) + +-- +-- Parsing +-- + +parseAddable :: + ( forall sem. syn sem => Addable sem + , syn (ForallSem syn) + ) => + (TermAST -> Parser syn) -> + TermAST -> + Parser syn +parseAddable _final (BinTree0 (TokenTermAtom s)) + | Right (i :: Int) <- safeRead s = + Parser $ Right $ TermVT TyConst{tyConst = Const{constType = typeRep, constMeta = ()}, tyConstLen = LenZ} $ ForallSem @_ @Int $ lit i +parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $ + case final aT of + Parser aE -> do + TermVT aTy (ForallSem a :: ForallSem syn a) <- aE + case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of + Nothing -> Left "TypeError" + Just HRefl -> do + Right $ TermVT aTy $ neg a +parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) = + Parser $ do + TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT) + case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of + Nothing -> Left "TypeError" + Just HRefl -> do + TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT) + case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of + Nothing -> Left "TypeError" + Just HRefl -> do + Right $ TermVT aTy $ ForallSem @_ @Int $ add a b +parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e + +-- tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int) +-- tree0Parser = unParser $ parse tree0Print + +parseMulable :: + ( forall sem. syn sem => Mulable sem + , forall sem. syn sem => Addable sem + , syn (ForallSem syn) + ) => + (TermAST -> Parser syn) -> + TermAST -> + Parser syn +parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) = + Parser $ do + case (final aT, final bT) of + (Parser aE, Parser bE) -> do + TermVT aTy (ForallSem a :: ForallSem syn a) <- aE + case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar aTy} of + Nothing -> Left "TypeError" + Just HRefl -> do + TermVT bTy (ForallSem b :: ForallSem syn b) <- bE + case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = ()}, tyConstLen = lenVar bTy} of + Nothing -> Left "TypeError" + Just HRefl -> do + Right $ TermVT aTy (ForallSem @_ @a $ mul a b) +parseMulable final t = parseAddable final t + +parseAbstractable :: + ( forall sem. syn sem => Mulable sem + , forall sem. syn sem => Addable sem + , forall sem. syn sem => Abstractable sem + , syn (ForallSem syn) + ) => + a ~ Int => + (TermAST -> Parser syn) -> + TermAST -> + Parser syn +-- TODO: parse variables +parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy :: Ty meta vs a)) bT)) = + Parser $ + case final bT of + Parser bE -> do + TermVT abTy (abF :: ForallSem syn ab) <- bE + case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar aTy} aTy of + Nothing -> Left "TypeError" + Just HRefl -> do + case abTy of + FUN iTy bTy -> + case eqTy TyConst{tyConst = Const{constType = typeRep @Type, constMeta = ()}, tyConstLen = lenVar bTy} bTy of + Nothing -> Left "TypeError" + Just HRefl -> do + let (aTy', iTy') = appendVars aTy iTy + case eqTy aTy' iTy' of + Nothing -> Left "TypeError" + Just HRefl -> do + case abF of + ForallSem ab -> + Right $ + TermVT abTy $ + ForallSem @_ @ab $ + -- FIXME: Tyable + lam (ab .@) + _ -> Left "TypeError" +parseAbstractable final t = parseMulable final t + +-- +-- Printing +-- + +instance Addable Printer where + lit n = Printer $ BinTree0 (TokenTermAtom (show n)) + neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT + add = print2 "Add" +instance Mulable Printer where + mul = print2 "Mul" +instance Abstractable Printer where + Printer f .@ Printer a = Printer $ BinTree2 f a + lam (f :: Printer a -> Printer b) = + Printer $ + -- FIXME: Tyable? instead of Typeable? + BinTree0 + ( TokenTermAbst + "x" + (TyVT TyConst{tyConst = Const{constType = typeRep @a, constMeta = ()}, tyConstLen = LenZ}) + (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x"))))) + ) + +class (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem +instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem + +fix :: (a -> a) -> a +fix f = f (fix f) + +parse :: + ( forall sem. syn sem => Addable sem + , forall sem. syn sem => Mulable sem + , forall sem. syn sem => Abstractable sem + , syn (ForallSem syn) + ) => + TermAST -> + Parser syn +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))) +tree0Print = print tree0 +tree1Print = print tree1 +tree2Print = print tree2 + +tree0ParsePrint :: TermAST +tree0ParsePrint = case parse @FinalSyntaxes tree0Print of + Parser (Left e) -> error e + Parser (Right (TermVT _ty (ForallSem sem))) -> print sem + +tree1ParsePrint :: TermAST +tree1ParsePrint = case parse @FinalSyntaxes tree1Print of + Parser (Left e) -> error e + Parser (Right (TermVT _ty (ForallSem sem))) -> print sem + +tree2ParsePrint :: TermAST +tree2ParsePrint = case parse @FinalSyntaxes tree2Print of + Parser (Left e) -> error e + Parser (Right (TermVT _ty (ForallSem sem))) -> print sem diff --git a/src/Symantic/Typer.hs b/src/Symantic/Typer.hs new file mode 100644 index 0000000..1a2a16d --- /dev/null +++ b/src/Symantic/Typer.hs @@ -0,0 +1,11 @@ +module Symantic.Typer ( + module Symantic.Typer.Type, + module Symantic.Typer.List, + module Symantic.Typer.Unify, + module Symantic.Typer.Eq, +) where + +import Symantic.Typer.Eq +import Symantic.Typer.List +import Symantic.Typer.Type +import Symantic.Typer.Unify diff --git a/src/Symantic/Typer/Eq.hs b/src/Symantic/Typer/Eq.hs new file mode 100644 index 0000000..b2cc9ba --- /dev/null +++ b/src/Symantic/Typer/Eq.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE PolyKinds #-} + +module Symantic.Typer.Eq where + +import Data.Kind (Type) +import Data.Maybe (Maybe (..)) +import Type.Reflection ((:~~:) (..)) + +class EqTy (x :: xK -> Type) (y :: yK -> Type) where + -- | /Heterogeneous type equality/: + -- return two proofs when two types are equals: + -- one for the type and one for the kind. + eqTy :: x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT) diff --git a/src/Symantic/Typer/List.hs b/src/Symantic/Typer/List.hs new file mode 100644 index 0000000..9ac5b7c --- /dev/null +++ b/src/Symantic/Typer/List.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE PolyKinds #-} + +module Symantic.Typer.List where + +import Data.Function (($), (.)) +import Data.Int (Int) +import Text.Show (Show (..)) +import Prelude qualified + +-- * Type family @(++)@ +type family (++) xs ys where + '[] ++ ys = ys + -- xs ++ '[] = xs + (x ': xs) ++ ys = x ': xs ++ ys +infixr 5 ++ + +-- * Type 'Len' +data Len (xs :: [k]) where + LenZ :: Len '[] + LenS :: Len xs -> Len (x ': xs) + +instance Show (Len vs) where + showsPrec _p = showsPrec 10 . intLen + +addLen :: Len a -> Len b -> Len (a ++ b) +addLen LenZ b = b +addLen (LenS a) b = LenS $ addLen a b + +shiftLen :: forall t b a. Len a -> Len (a ++ b) -> Len (a ++ t ': b) +shiftLen LenZ b = LenS b +shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b + +intLen :: Len xs -> Int +intLen = go 0 + where + go :: Int -> Len xs -> Int + go i LenZ = i + go i (LenS l) = go (1 Prelude.+ i) l + +-- ** Class 'LenInj' +class LenInj (vs :: [k]) where + lenInj :: Len vs +instance LenInj '[] where + lenInj = LenZ +instance LenInj as => LenInj (a ': as) where + lenInj = LenS lenInj diff --git a/src/Symantic/Typer/Type.hs b/src/Symantic/Typer/Type.hs new file mode 100644 index 0000000..68e2754 --- /dev/null +++ b/src/Symantic/Typer/Type.hs @@ -0,0 +1,467 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-partial-fields #-} + +module Symantic.Typer.Type where + +import Control.Applicative (Applicative (..), liftA3) +import Control.Monad (Monad (..), sequence) +import Control.Monad.Classes as MC () +import Control.Monad.Classes.Run as MC () +import Control.Monad.Trans.Except qualified as MT +import Control.Monad.Trans.Identity (IdentityT (..)) +import Control.Monad.Trans.Reader qualified as MT +import Control.Monad.Trans.State qualified as MT +import Control.Monad.Trans.Writer.CPS qualified as MT +import Data.Bool (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.Int (Int) +import Data.Kind (Constraint, Type) +import Data.Map.Strict qualified as Map +import Data.Maybe (Maybe (..), isJust) +import Data.Monoid (Monoid (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (Semigroup (..)) +import Data.Set qualified as Set +import Data.String (String) +import GHC.Types +import Text.Read (Read (..), reads) +import Text.Show (Show (..)) +import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..)) +import Unsafe.Coerce (unsafeCoerce) +import Prelude (error) +import Prelude qualified + +import Symantic.Parser.Source +import Symantic.Typer.Eq +import Symantic.Typer.List + +data Const meta a = Const + { constType :: TypeRep a + , constMeta :: meta + } + deriving (Show) +instance EqTy (Const meta) (Const meta) where + eqTy Const{constType = x} Const{constType = y} = eqTypeRep x y + +type Name = String + +-- * Type 'Var' +data Var :: forall vK. Type -> [Type] -> vK -> Type where + VarZ :: + { varZKind :: Kind meta vK + , varZNext :: Len ws + , varZMeta :: meta + } -> + Var meta (Proxy (v :: vK) ': ws) (v :: vK) + VarS :: Var meta vs v -> Var meta (not_v ': vs) v +deriving instance Show meta => Show (Var meta vs v) + +pattern Var :: () => () => Kind meta vK -> Len ws -> meta -> Var meta vs' (v :: vK) +pattern Var{varKind, varNext, varMeta} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext, varZMeta = varMeta}) +{-# COMPLETE Var #-} + +-- -- * Type 'VarVS' +data VarVS meta (v :: vK) = forall vs. VarVS (Var meta vs v) +var :: Var meta vs (v :: vK) -> VarVS meta (v :: vK) +var v@VarZ{} = VarVS v +var (VarS v) = var v + +instance EqTy (Var meta vs) (Var meta vs) where + eqTy VarZ{} VarZ{} = Just HRefl + eqTy (VarS x) (VarS y) = eqTy x y + eqTy _ _ = Nothing + +type VarSem = Type -> [Type] -> Type -> Type + +-- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v) +data VarV meta vs = forall v. VarV (Var meta vs v) + +class LenVar var where + lenVar :: var meta vs a -> Len vs +instance LenVar Var where + lenVar VarZ{varZNext} = LenS varZNext + lenVar (VarS v) = LenS (lenVar v) + +class LenVar var => AllocVars var where + allocVarsL :: Len len -> var meta vs x -> var meta (len ++ vs) x + allocVarsR :: Len len -> var meta vs x -> var meta (vs ++ len) x +instance AllocVars Var where + allocVarsL LenZ v = v + allocVarsL (LenS len) v = VarS (allocVarsL len v) + + allocVarsR len VarZ{..} = VarZ{varZNext = addLen varZNext len, ..} + allocVarsR len (VarS v) = VarS (allocVarsR len v) + +appendVars :: + AllocVars xVar => + AllocVars yVar => + xVar meta xVS (x :: xK) -> + yVar meta yVS (y :: yK) -> + ( xVar meta (xVS ++ yVS) x + , yVar meta (xVS ++ yVS) y + ) +appendVars x y = + ( allocVarsR (lenVar y) x + , allocVarsL (lenVar x) y + ) + +-- ** Type 'IndexVar' + +-- | Index of a 'Var'. +type IndexVar = Int + +indexVar :: Var meta vs v -> Int +indexVar VarZ{} = 0 +indexVar (VarS v) = 1 Prelude.+ indexVar v + +-- instance KindOf (Var meta vs) where +-- kindOf = fmap go +-- where +-- go :: forall vs2 aK a. Var meta vs2 (Proxy (a::aK)) -> TypeRep aK +-- go VarZ{varKind} = varKind +-- go (VarS v) = go v + +-- * Type 'Vars' +type Vars meta vs = Map.Map Name (VarV meta vs) + +lookupVar :: Name -> Vars meta vs -> Maybe (VarV meta vs) +lookupVar = Map.lookup + +insertVar :: Name -> VarV meta vs -> Vars meta vs -> Vars meta vs +insertVar = Map.insert + +-- * Type 'UsedVars' + +-- | List of 'Var's, used to change the context of a 'Var' +-- when removing unused 'Var's. +data UsedVars oldVS meta newVS a where + UsedVarsZ :: UsedVars oldVS meta '[] a + UsedVarsS :: + Var meta oldVS (v :: vK) -> + UsedVars oldVS meta newVS a -> + UsedVars oldVS meta (Proxy (v :: vK) ': newVS) a + +instance LenVar (UsedVars oldVS) where + lenVar UsedVarsZ = LenZ + lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS + +lookupUsedVars :: + Var meta oldVS (v :: vK) -> + UsedVars oldVS meta newVS a -> + Maybe (Var meta newVS (v :: vK)) +lookupUsedVars _v UsedVarsZ = Nothing +lookupUsedVars v (UsedVarsS v' us) = do + case v `eqTy` v' of + Just HRefl -> + case v' of + Var{varKind, varMeta} -> + Just + VarZ + { varZNext = lenVar us + , varZKind = varKind + , varZMeta = varMeta + } + Nothing -> VarS Data.Functor.<$> lookupUsedVars v us + +insertUsedVars :: + Var meta vs v -> + UsedVars vs meta us a -> + Maybe (UsedVars vs meta (Proxy v ': us) a) +insertUsedVars v vs = + case lookupUsedVars v vs of + Just{} -> Nothing + Nothing -> Just (UsedVarsS v vs) + +-- * Class 'VarOccursIn' + +-- | Test whether a given 'Var' occurs within @(t)@. +class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where + varOccursIn :: Var meta vs v -> t meta vs a -> Bool + +-- * Class 'UsedVarsOf' +class UsedVarsOf t where + usedVarsOf :: + UsedVars vs meta oldVS a -> + t meta vs b -> + (forall newVS. UsedVars vs meta newVS a -> ret) -> + ret + +-- * Type 'Ty' + +-- Use a CUSK, because it's a polymorphically recursive type, +-- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/ +data Ty :: forall aK. Type -> [Type] -> aK -> Type where + TyConst :: {tyConst :: Const meta a, tyConstLen :: Len vs} -> Ty meta vs a + TyVar :: {tyVar :: Var meta vs a, tyVarName :: Name} -> Ty meta vs a + TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a) +infixl 9 `TyApp` + +pattern FUN :: + -- CReq + forall k (fun :: k) meta vs. + () => + {-Monoid meta-} + -- CProv + forall + (r1 :: RuntimeRep) + (r2 :: RuntimeRep) + (arg :: TYPE r1) + (res :: TYPE r2). + ( k ~ Type + , fun ~~ (arg -> res) + -- , r1 ~ LiftedRep + -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -} + ) => + Ty meta vs arg -> + Ty meta vs res -> + Ty meta vs fun +pattern FUN arg res <- + TyApp + { tyAppFun = + TyApp + { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}} + , tyAppArg = arg + } + , tyAppArg = res + } + +-- where FUN arg res = +-- TyApp +-- { tyAppFun = TyApp +-- { tyAppFun = TyConst +-- { tyConstLen=lenVar arg +-- , tyConst=Const{ constType=typeRep @(->) +-- , constMeta=(mempty::meta)} +-- } +-- , tyAppArg = arg +-- } +-- , tyAppArg = res +-- } + +deriving instance Show meta => Show (Ty meta vs a) + +-- type instance SourceOf (Ty vs src t) = src +instance LenVar Ty where + lenVar TyConst{tyConstLen} = tyConstLen + lenVar TyApp{tyAppFun} = lenVar tyAppFun + lenVar TyVar{tyVar} = lenVar tyVar + +-- lenVars (TyFam l _f _as) = l +instance AllocVars Ty where + allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen} + allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg} + allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar} + + -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as + + allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len} + allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..} + allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar} + +-- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as +instance VarOccursIn Ty where + varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False + varOccursIn _v TyVar{} = False + varOccursIn _v TyConst{} = False + varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a + +-- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as +instance UsedVarsOf Ty where + usedVarsOf vs TyConst{} k = k vs + usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k = + usedVarsOf vs f $ \vs' -> + usedVarsOf vs' a k + usedVarsOf vs TyVar{tyVar = v} k = + case insertUsedVars v vs of + Nothing -> k vs + Just vs' -> k vs' + +-- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k + +-- ** Type 'TyT' + +-- | Existential for 'Type'. +data TyT meta vs = forall a. TyT (Ty meta vs a) + +-- type instance SourceOf (TyT vs src) = src +instance Eq (TyT meta vs) where + TyT x == TyT y = isJust $ eqTy x y +instance Show meta => Show (TyT meta vs) where + showsPrec p (TyT x) = showsPrec p x + +-- * Type 'Kind' +type Kind meta a = Ty meta '[] a + +-- ** Type 'KindK' +type KindK meta = TyT meta '[] + +-- ** Type 'TyVT' +data TyVT meta = forall vs a. TyVT (Ty meta vs a) + +deriving instance Show meta => Show (TyVT meta) +instance Eq (TyVT m) where + TyVT x == TyVT y = isJust (eqTy x' y') + where + (x', y') = appendVars x y + +-- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where +-- eqTy x y = eqTy (unSourced x) (unSourced y) +instance EqTy (Ty meta vs) (Ty meta vs) where + eqTy TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y + eqTy TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y + eqTy TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA} + | Just HRefl <- eqTy xF yF + , Just HRefl <- eqTy xA yA = + Just HRefl + eqTy _x _y = Nothing + +-- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA) +-- | Just HRefl <- eqTypeRep xF yF +-- , Just HRefl <- eqTys xA yA +-- = Just HRefl +-- -- NOTE: 'TyFam' is expanded as much as possible. +-- eqTy x@TyFam{} y = eqTy (expandFam x) y +-- eqTy x y@TyFam{} = eqTy x (expandFam y) + +-- * Type 'Tys' +data Tys (as :: [Type]) meta vs (a :: aK) where + TysZ :: Tys '[] meta vs a + TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b +infixr 5 `TysS` + +-- type instance SourceOf (Tys vs src ts) = src +-- instance ConstsOf (Tys meta vs ts) where +-- constsOf TysZ = Set.empty +-- constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts +instance UsedVarsOf (Tys as) where + usedVarsOf vs TysZ k = k vs + usedVarsOf vs (TysS t ts) k = + usedVarsOf vs t $ \vs' -> + usedVarsOf vs' ts k +instance VarOccursIn (Tys as) where + varOccursIn _v TysZ = False + varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts + +-- ** Type family 'FunArg' +type family FunArg (fun :: Type) :: Type where + FunArg (q #> f) = FunArg f + FunArg (a -> b) = a + +-- ** Type family 'FunRes' +type family FunRes (fun :: Type) :: Type where + FunRes (q #> f) = FunRes f + FunRes (a -> b) = b + +-- -- | Return, when the given 'Type' is a function, +-- -- the argument of that function. +-- unTyFun :: +-- forall t src tys. +-- SourceInj (TyVT src) src => +-- --Constable (->) => +-- Type src tys t -> +-- Maybe ( Type src tys (FunArg t) +-- , Type src tys (FunRes t) ) +-- unTyFun ty_ini = go ty_ini +-- where +-- go :: +-- Type src tys x -> +-- Maybe ( Type src tys (FunArg x) +-- , Type src tys (FunRes x) ) +-- go (TyApp _ (TyApp _ (TyConst _ _ f) a) b) +-- | Just HRefl <- proj_ConstKi @(K (->)) @(->) f +-- = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini)) +-- go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b) +-- | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f +-- = go b +-- go TyApp{} = Nothing +-- go TyConst{} = Nothing +-- go TyVar{} = Nothing +-- go TyFam{} = Nothing + +proj_ConstKi :: + forall kc (c :: kc) u meta. + Typeable c => + -- (kc ~ Type_of_Ty (Ty_of_Type kc)) => + -- KindInjP (Ty_of_Type kc) => + Const meta u -> + Maybe (c :~~: u) +proj_ConstKi = eqTypeRep (typeRep @c) . constType + +-- HRefl <- eqTy ku kc -- $ kindInjP @(Ty_of_Type kc) () +-- HRefl :: u:~~:c <- eqT +-- Just HRefl + +-- ** Type @(#>)@ + +-- | /Type constant/ to qualify a 'Type'. +newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a) + +-- | Qualify a 'Type'. +(#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t) +(#>) q t = + -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t + TyApp + { tyAppFun = + TyApp + { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q} + , tyAppArg = q + } + , tyAppArg = t + } + +infixr 0 #> + +-- NOTE: should actually be (-1) +-- to compose well with @infixr 0 (->)@ +-- but this is not allowed by GHC. + +-- ** Class @(#)@ + +-- | 'Constraint' union. +class ((x, y) :: Constraint) => x # y + +instance ((x, y) :: Constraint) => x # y + +-- | Unify two 'K.Constraint's. +(#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy) +(#) a b = + -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b + TyApp + { tyAppFun = + TyApp + { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a} + , tyAppArg = a + } + , tyAppArg = b + } + +infixr 2 # + +-- * Class 'KindOf' +class KindOf (ty :: Type -> [Type] -> aK -> Type) where + -- | Return the kind of the given 'Var'. + kindOf :: + -- Provenanceable (ProvenanceKindOf t) m => + -- MC.MonadWriter (ProvenanceKindOf t) m => + ty meta vs (a :: aK) -> + Kind meta aK + +instance KindOf Var where + kindOf Var{varKind} = varKind +instance KindOf Ty where + kindOf TyConst{tyConst = c} = TyConst{tyConst = c{constType = typeRepKind (constType c)}, tyConstLen = LenZ} + kindOf TyApp{tyAppFun = f} = case kindOf f of + FUN _ kf -> kf + kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind + +-- kindOf (TyFam _src _len fam _as) = kindOfConst fam diff --git a/src/Symantic/Typer/Unify.hs b/src/Symantic/Typer/Unify.hs new file mode 100644 index 0000000..0cf58c9 --- /dev/null +++ b/src/Symantic/Typer/Unify.hs @@ -0,0 +1,269 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Symantic.Typer.Unify where + +import Control.Monad (Monad (..)) +import Control.Monad.Classes as MC (MonadExcept, throw) +import Control.Monad.Classes.Run as MC () +import Data.Bool (otherwise) +import Data.Eq (Eq (..)) +import Data.Function (id, ($)) +import Data.Functor ((<$>)) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (Maybe (..)) +import Data.Monoid (Monoid (..)) +import Data.Semigroup (Semigroup (..)) +import Text.Show (Show) +import Type.Reflection ((:~~:) (..)) +import Unsafe.Coerce (unsafeCoerce) +import Prelude qualified + +-- import Symantic.Grammar +import Symantic.Typer.Variable () + +-- import Symantic.Typer.Kind + +import Symantic.Parser.Error (ErrorInj (..)) +import Symantic.Parser.Source (Source, SourceInj) +import Symantic.Typer.Eq (EqTy (eqTy)) +import Symantic.Typer.Type ( + IndexVar, + KindK, + KindOf (kindOf), + Ty (TyApp, TyConst, TyVar, tyConst, tyVar), + TyT (..), + TyVT (..), + Tys (..), + Var, + VarOccursIn (..), + indexVar, + proj_ConstKi, + type (#>), + ) + +-- import Symantic.Typer.Show () + +-- * Type 'Subst' + +-- | /Type variable substitution/. +-- +-- WARNING: a 'Subst' MUST be without loops, and fully expanded. +newtype Subst meta vs + = Subst (Map IndexVar (VT meta vs)) + +deriving instance (Show meta, Monoid meta) => Show (Subst meta vs) +instance Monoid meta => Semigroup (Subst meta vs) where + (<>) = unionSubst +instance Monoid meta => Monoid (Subst meta vs) where + mempty = Subst Map.empty + mappend = (<>) + +-- | Unify two 'Subst's. +-- +-- NOTE: the union is left-biased: in case of duplicate 'Var's, +-- it keeps the one from the first 'Subst' given. +-- +-- NOTE: the first 'Subst' given is applied to the second (with 'subst'), +-- this way each 'Var' directly maps to an expanded 'Type', +-- so that, when using the resulting 'Subst', +-- there is no need to apply it multiple times +-- until there is no more substitution to be done. +unionSubst :: Subst meta vs -> Subst meta vs -> Subst meta vs +unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) Data.Functor.<$> y) + +-- * Type 'VT' + +-- | A 'Var' and a 'Type' existentialized over their type index. +data VT meta vs = forall t. VT (Var meta vs t) (Ty meta vs t) + +deriving instance (Show meta, Monoid meta) => Show (VT meta vs) + +insertSubst :: Monoid meta => Var meta vs v -> Ty meta vs v -> Subst meta vs -> Subst meta vs +insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s + +lookupSubst :: Monoid meta => Var meta vs v -> Subst meta vs -> Maybe (Ty meta vs v) +lookupSubst v (Subst s) + | Just (VT v' t) <- Map.lookup (indexVar v) s + , Just Type.Reflection.HRefl <- v `eqTy` v' = + Just t +lookupSubst _v _m = Nothing + +-- * Class 'Substable' +class Substable t where + -- | Like 'substVar', but without the /occurence check/. + substVarUnsafe :: + Var meta vs v -> Ty meta vs v -> t meta vs a -> t meta vs a + + -- | Substitute all the 'Var's which have a match in given 'Subst'. + subst :: + Subst meta vs -> t meta vs a -> t meta vs a +instance Substable Ty where + substVarUnsafe _v _r t@TyConst{} = t + substVarUnsafe v r (TyApp f a) = + TyApp + (substVarUnsafe v r f) + (substVarUnsafe v r a) + substVarUnsafe v r t@TyVar{tyVar = tv} = + case v `eqTy` tv of + Just Type.Reflection.HRefl -> r + Nothing -> t + + -- substVarUnsafe v r (TyFam meta len fam as) = + -- TyFam meta len fam $ substVarUnsafe v r as + + subst _s t@TyConst{} = t + subst s (TyApp f a) = TyApp (subst s f) (subst s a) + subst (Subst s) t@TyVar{tyVar = tv} = + case Map.lookup (indexVar tv) s of + Nothing -> t + Just (VT vr r) -> + case tv `eqTy` vr of + Nothing -> Prelude.error "[BUG] subst: kind mismatch" + Just Type.Reflection.HRefl -> r + +-- subst s (TyFam meta len fam as) = TyFam meta len fam $ subst s as +instance Substable (Tys as) where + substVarUnsafe _v _r TysZ = TysZ + substVarUnsafe v r (TysS t ts) = + substVarUnsafe v r t + `TysS` substVarUnsafe v r ts + subst _s TysZ = TysZ + subst s (TysS t ts) = subst s t `TysS` subst s ts + +-- | Substitute the given 'Var' by the given 'Type', +-- returning 'Nothing' if this 'Type' contains +-- the 'Var' (occurence check). +substVar :: + VarOccursIn t => + Substable t => + Var meta vs v -> + Ty meta vs v -> + t meta vs a -> + Maybe (t meta vs a) +substVar v r t = + if v `varOccursIn` r + then Nothing -- NOTE: occurence check + else Just $ substVarUnsafe v r t + +-- ** Type 'ErrorUnify' + +-- | Reasons why two 'Type's cannot be unified. +data ErrorUnify meta + = -- | /occurence check/: a 'Var' is unified with a 'Type' + -- which contains this same 'Var'. + ErrorUnifyVarLoop IndexVar (TyVT meta) + | -- | Two 'TyConst's should be the same, but are different. + ErrorUnifyConst (TyVT meta) (TyVT meta) + | -- | Two 'Kind's should be the same, but are different. + ErrorUnifyKind (KindK meta) (KindK meta) + | -- | Cannot unify those two 'Type's. + ErrorUnifyType (TyVT meta) (TyVT meta) + +deriving instance Monoid meta => Eq (ErrorUnify meta) +deriving instance (Show meta, Monoid meta) => Show (ErrorUnify meta) + +instance ErrorInj (ErrorUnify meta) (ErrorUnify meta) where + errorInj = id + +data SourceTypeArg meta + = SourceTypeArg (TyVT meta) + +-- | Return the left spine of a 'Ty': +-- the root 'Ty' and its 'Ty' parameters, +-- from the left to the right. +spineTy :: + forall meta vs t. + -- MC.MonadWriter (SourceTypeArg meta) (Sourced meta) => + Source meta => + SourceInj (TyVT meta) meta => + Ty meta vs t -> + (TyT meta vs, [TyT meta vs]) +spineTy = go [] + where + go :: forall kx (x :: kx). [TyT meta vs] -> Ty meta vs x -> (TyT meta vs, [TyT meta vs]) + -- Skip the constraint @q@. + go ctx (TyApp (TyApp (TyConst{tyConst = c}) _q) t) + | Just Type.Reflection.HRefl <- proj_ConstKi @_ @(#>) c = + go ctx t + -- Add a type to the spine. + go ctx (TyApp f a) = go (TyT a {-(SourceTypeArg (TyVT ty)-} : ctx) f + -- Add the root. + go ctx t = (TyT t {-SourceTypeArg (TyVT ty)-}, ctx) + +{- +spineTy + :: Ty meta ctx ss cs (t::k) + -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret) + -> ret +spineTy = go TysZ + where + go :: Tys meta ctx ss cs hs + -> Ty meta ctx ss cs (t::k) + -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret) + -> ret + go ctx (TyApp _src f a) k = go (a `TysS` ctx) f k + go ctx (Term x _te) k = go ctx x k + go ctx (TyAny x) k = go ctx x k + go ctx t k = k t ctx +-} + +-- | Return the /most general unification/ of two 'Type's, when it exists. +unifyType :: + forall ki (x :: ki) (y :: ki) vs meta m. + SourceInj (TyVT meta) meta => + -- ErrorInj (Con_Kind meta) (ErrorUnify meta) => + MC.MonadExcept (ErrorUnify meta) m => + Subst meta vs -> + Ty meta vs (x :: ki) -> + Ty meta vs (y :: ki) -> + m (Subst meta vs) +unifyType vs x y = + let k = kindOf x + in case (spineTy x, spineTy y) of + ((TyT xRootTy, px), (TyT yRootTy, py)) -> + case (xRootTy, yRootTy) of + (TyVar{tyVar = vx}, _) | Just Type.Reflection.HRefl <- k `eqTy` kindOf vx -> goVar vs vx y + (_, TyVar{tyVar = vy}) | Just Type.Reflection.HRefl <- k `eqTy` kindOf vy -> goVar vs vy x + (TyConst{tyConst = cx}, TyConst{tyConst = cy}) + | Just Type.Reflection.HRefl <- cx `eqTy` cy -> goZip vs px py + | otherwise -> MC.throw $ ErrorUnifyConst (TyVT xRootTy) (TyVT yRootTy) + _ -> + case (x, y) of + (TyApp fx ax, TyApp fy ay) -> goZip vs [TyT fx, TyT ax] [TyT fy, TyT ay] + _ -> MC.throw $ ErrorUnifyType (TyVT x) (TyVT y) + where + goVar :: + forall k (a :: k) (b :: k) vs'. + Subst meta vs' -> + Var meta vs' a -> + Ty meta vs' b -> + m (Subst meta vs') + goVar vs' va b = + case va `lookupSubst` vs' of + Just a -> unifyType vs' b a + Nothing -> + case vs' `subst` b of + TyVar{tyVar = vb} | Just Type.Reflection.HRefl <- va `eqTy` vb -> return vs' + b' + | va `varOccursIn` b' -> MC.throw $ ErrorUnifyVarLoop (indexVar va) (TyVT b') + | Type.Reflection.HRefl :: a Type.Reflection.:~~: b <- unsafeCoerce Type.Reflection.HRefl -> + return $ insertSubst va b' mempty <> vs' + goZip :: + forall vs'. + Subst meta vs' -> + [TyT meta vs'] -> + [TyT meta vs'] -> + m (Subst meta vs') + goZip vs' [] [] = return vs' + goZip vs' (TyT a : as) (TyT b : bs) = + let xK = kindOf a + in let yK = kindOf b + in case xK `eqTy` yK of + Nothing -> MC.throw $ ErrorUnifyKind (TyT xK) (TyT yK) + Just Type.Reflection.HRefl -> unifyType vs' a b >>= \vs'' -> goZip vs'' as bs + goZip _vs _a _b = Prelude.error "[BUG] unifyType: kinds mismatch" diff --git a/symantic.cabal b/symantic.cabal index 4c0004d..8b59ff2 100644 --- a/symantic.cabal +++ b/symantic.cabal @@ -1,35 +1,26 @@ cabal-version: 3.0 -name: literate-web -maintainer: mailto:literate-web@sourcephile.fr -bug-reports: https://mails.sourcephile.fr/inbox/literate-web -homepage: https://git.sourcephile.fr/literate-web.git -author: Julien Moutinho <julm+literate-web@sourcephile.fr> -copyright: Julien Moutinho <julm+literate-web@sourcephile.fr> +name: symantic +maintainer: mailto:symantic@sourcephile.fr +bug-reports: https://mails.sourcephile.fr/inbox/symantic +homepage: https://git.sourcephile.fr/symantic.git +author: Julien Moutinho <julm+symantic@sourcephile.fr> +copyright: Julien Moutinho <julm+symantic@sourcephile.fr> license: AGPL-3.0-or-later license-file: LICENSES/AGPL-3.0-or-later.txt -- PVP: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change -version: 0.0.0.20221117 +version: 0.0.0.20230723 stability: experimental -category: Web +category: Language synopsis: Haskell-website compiler description: - Exploring the design space of compile-time website generator - by using a domain-specific language (DSL) - embedded into the Haskell language. - . - Alternatives: - . - * <https://hackage.haskell.org/package/ema ema> - build-type: Simple tested-with: GHC ==9.2.4 extra-doc-files: ChangeLog.md extra-source-files: .envrc - cabal.project flake.lock flake.nix @@ -37,7 +28,7 @@ extra-tmp-files: source-repository head type: git - location: git://git.sourcephile.fr/haskell/literate-web.git + location: git://git.sourcephile.fr/haskell/symantic.git common boilerplate default-language: Haskell2010 @@ -70,6 +61,8 @@ common boilerplate -Wmonomorphism-restriction -Wpartial-fields -fprint-potential-instances +-- -fprint-explicit-kinds + -- -dshow-passes -- -ddump-to-file -- -ddump-simpl @@ -81,169 +74,28 @@ common boilerplate common library-deps build-depends: - , async >=2.2 - , base >=4.6 && <5 - , bytestring >=0.10 - , containers >=0.5 - , directory >=1.3 - , filepath >=1.4 - , filepattern >=0.1 - , hashable - , http-client >=0.6 - , http-media >=0.7 + , base >=4.6 && <5 + , containers >=0.5 + , ghc-prim , monad-classes - , peano - , reflection - , symantic-base >=0.5 - , template-haskell + , symantic-base >=0.5 , text - , transformers >=0.5 - , unicode-transforms >=0.2 - , unordered-containers - , uri-encode >=1.5 - , wai - , wai-middleware-static - , wai-websockets - , warp - , websockets >=0.12 - , pipes - , pipes-safe - , pipes-concurrency - , pipes-parse - , pipes-group - , mvc - , mvc-updates - , ghc-prim + , transformers + , vector library import: boilerplate, library-deps hs-source-dirs: src exposed-modules: - ForallSem - Literate.Web - Literate.Web.Semantics.Compiler - Literate.Web.Semantics.Addresser - Literate.Web.Syntaxes - Literate.Web.Types.MIME - Literate.Web.Types.URL - -library relactive - import: boilerplate, library-deps - hs-source-dirs: src - build-depends: - , async - , contravariant >=1.5 - , stm - , monad-classes - - exposed-modules: - Control.Reactive - Control.Reactive.IORef - Control.Reactive.MVar - Control.Reactive.Relation - Control.Reactive.STRef - Control.Reactive.TVar - Control.Reactive.Value - --- Literate.Web.Semantics.Server --- Literate.Web.Semantics.Client ---Literate.Web.Decoder ---Literate.Web.Encoder ---Literate.Web.Generator ---Literate.Web.MIME - ---Literate.Web.Decoder -test-suite literate-web-tests - -- library-deps is only to have ghcid reloaded on changes in src - import: boilerplate, library-deps - type: exitcode-stdio-1.0 - hs-source-dirs: tests - main-is: Main.hs - other-modules: - Examples.Ex01 - Examples.Ex02 - Examples.Ex03 - Examples.Ex04 - Examples.Ex05 - Goldens - Paths_literate_web - Utils - autogen-modules: Paths_literate_web - build-depends: - , base >=4.6 && <5 - , containers >=0.5 - , literate-web - , monad-classes - , relude - , symantic-base >=0.5 - , tasty >=0.11 - , tasty-golden >=2.3 - , tasty-hunit >=0.9 - , text >=1.2 - , transformers >=0.5 - , relactive - --- , relude >=1 && <2 -benchmark time - import: boilerplate, library-deps - type: exitcode-stdio-1.0 - hs-source-dirs: benchmarks/time - main-is: Main.hs - build-depends: - , base >=4.6 && <5 - , relactive - , tasty - , tasty-bench - - -- , relude >= 1 - -- Set a larger allocation area (nursery) - -- to remove some noisiness of the garbage collection. - ghc-options: -with-rtsopts=-A32m - -benchmark weigh - import: boilerplate, library-deps - type: exitcode-stdio-1.0 - hs-source-dirs: benchmarks/weigh src - build-depends: - , async - , contravariant >=1.5 - , stm - - main-is: Main.hs - build-depends: - , base >=4.6 && <5 - , relude >=1 - , weigh - ---, relactive -executable async - import: boilerplate, library-deps - hs-source-dirs: executables/async - main-is: Main.hs - build-depends: - , async - , base >=4.6 && <5 - , relactive - , relude - , symantic-base - , tasty - , tasty-bench - --- , relude >= 1 - -executable fsnotify - import: boilerplate, library-deps - hs-source-dirs: executables/fsnotify - main-is: Main.hs - build-depends: - , async - , base >=4.6 && <5 - , directory - , filepath - , fsnotify - , relactive - , relude >=1 - , symantic-base - , tasty - , tasty-bench - , time + Symantic.Compiler + Symantic.Compiler.Term + Symantic.Parser + Symantic.Parser.Error + Symantic.Parser.Source + Symantic.Printer + Symantic.Syntaxes + Symantic.Typer + Symantic.Typer.Eq + Symantic.Typer.List + Symantic.Typer.Type + Symantic.Typer.Unify -- 2.47.2