wip: Implement typesystem

covenant.cabal

@@ -88,6 +88,8 @@ library
   other-modules:
     Covenant.Internal.ASGBuilder
     Covenant.Internal.ASGNode
+    Covenant.Internal.PrimType
+
 
   build-depends:
     QuickCheck ==2.15.0.1,

src/Covenant/ASG.hs

@@ -27,6 +27,8 @@ module Covenant.ASG
     ASGBuilder,
     Scope,
     ASG,
+    ASGBuilderError (..),
+    TypeError (..),
 
     -- * Functions
     emptyScope,
@@ -51,27 +53,38 @@ import Algebra.Graph.Acyclic.AdjacencyMap
     vertex,
   )
 import Algebra.Graph.AdjacencyMap qualified as Cyclic
-import Control.Monad.State.Strict (runState)
 import Covenant.Internal.ASGBuilder
-  ( ASGBuilder (ASGBuilder),
+  ( ASGBuilder,
+    ASGBuilderError (ATypeError),
     ASGBuilderState (ASGBuilderState),
+    TypeError
+      ( TyErrAppArgMismatch,
+        TyErrAppNotALambda,
+        TyErrNonHomogenousList,
+        TyErrPrimArgMismatch
+      ),
     app,
     idOf,
     lit,
     prim,
+    runASGBuilder,
   )
 import Covenant.Internal.ASGNode
   ( ASGNode (App, Lam, Let, Lit, Prim),
+    ASGType (TyLam),
     Arg (Arg),
     Bound (Bound),
     Id,
     PrimCall (PrimCallOne, PrimCallSix, PrimCallThree, PrimCallTwo),
     Ref (ABound, AnArg, AnId),
+    typeOfRef,
   )
 import Data.Bimap (Bimap)
 import Data.Bimap qualified as Bimap
-import Data.Maybe (mapMaybe)
+import Data.Maybe (fromJust, mapMaybe)
 import Data.Proxy (Proxy (Proxy))
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
 import GHC.TypeNats (CmpNat, KnownNat, natVal, type (+))
 import Numeric.Natural (Natural)
 
@@ -90,20 +103,21 @@ data ASG = ASG (Id, ASGNode) (AdjacencyMap (Id, ASGNode))
 -- refers to into a call graph. This is guaranteed to be acyclic.
 --
 -- @since 1.0.0
-toASG :: ASGBuilder Id -> Maybe ASG
-toASG (ASGBuilder comp) = do
-  let (start, ASGBuilderState binds) = runState comp (ASGBuilderState Bimap.empty)
+toASG :: ASGBuilder Id -> Either ASGBuilderError ASG
+toASG comp = do
+  let (startOrError, ASGBuilderState (binds :: Bimap Id ASGNode)) = runASGBuilder comp (ASGBuilderState Bimap.empty)
+  start :: Id <- startOrError
   if Bimap.size binds == 1
     then do
-      -- This cannot fail, but the type system can't show it
-      initial <- (start,) <$> Bimap.lookup start binds
+      let -- This cannot fail, but the type system can't show it
+          initial = (start, (Bimap.!) binds start)
       pure . ASG initial . vertex $ initial
     else do
       let asGraph = Cyclic.edges . go binds $ start
-      -- This cannot fail, but the type system can't show it
-      acyclic <- toAcyclic asGraph
-      -- Same as above
-      initial <- (start,) <$> Bimap.lookup start binds
+          -- This cannot fail, but the type system can't show it
+          acyclic = fromJust $ toAcyclic asGraph
+          -- Same as above
+          initial = (start, (Bimap.!) binds start)
       pure . ASG initial $ acyclic
   where
     go ::
@@ -125,7 +139,7 @@ toASG (ASGBuilder comp) = do
 -- bindings (each with a bound variable we can refer to.
 --
 -- @since 1.0.0
-data Scope (args :: Natural) (lets :: Natural) = Scope
+data Scope (args :: Natural) (lets :: Natural) = Scope (Vector ASGType) (Vector ASGType)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -137,7 +151,7 @@ data Scope (args :: Natural) (lets :: Natural) = Scope
 --
 -- @since 1.0.0
 emptyScope :: Scope 0 0
-emptyScope = Scope
+emptyScope = Scope Vector.empty Vector.empty
 
 -- | Given a proof of scope, construct one of the arguments in that scope. This
 -- requires use of @TypeApplications@ to select which argument you are
@@ -153,7 +167,11 @@ arg ::
   (KnownNat n, CmpNat n m ~ LT) =>
   Scope m lets ->
   Arg
-arg Scope = Arg . fromIntegral . natVal $ Proxy @n
+arg (Scope args _) =
+  let n = natVal $ Proxy @n
+      -- This cannot fail, but the type system can't show it
+      argTy = (Vector.!) args (fromIntegral n)
+   in Arg (fromIntegral n) argTy
 
 -- | Given a proof of scope, construct one of the @let@-bound variables in that
 -- scope. This requires use of @TypeApplications@ to select which bound variable
@@ -169,28 +187,40 @@ bound ::
   (KnownNat n, CmpNat n m ~ LT) =>
   Scope args m ->
   Bound
-bound Scope = Bound . fromIntegral . natVal $ Proxy @n
+bound (Scope _ lets) =
+  let n = natVal $ Proxy @n
+      -- This cannot fail, but the type system can't show it
+      letTy = (Vector.!) lets (fromIntegral n)
+   in Bound (fromIntegral n) letTy
 
--- | Given a proof of scope, and a function to construct a lambda body using a
--- \'larger\' proof of scope, construct a lambda with that body.
+-- | Given the type of the lambda argument and a proof of scope, and a function
+-- to construct a lambda body using a \'larger\' proof of scope, construct a
+-- lambda with that body.
 --
+-- Note (Farseen, 2025\/02\/11): Update this example once parametric polymorphism is implemented.
 -- For example, this is how you define @id@:
 --
 -- > lam emptyScope $ \s10 -> pure . AnArg $ arg @0 s10
 --
+-- Note (Farseen, 2025\/02\/11): Update this example once parametric polymorphism is implemented.
 -- This is @const@:
 --
 -- > lam emptyScope $ \s10 -> lam s10 $ \s20 -> pure . AnArg $ arg @1 s20
 --
 -- @since 1.0.0
 lam ::
   forall (n :: Natural) (m :: Natural).
+  -- | The type of the lambda argument
+  ASGType ->
   Scope n m ->
   (Scope (n + 1) m -> ASGBuilder Ref) ->
   ASGBuilder Id
-lam Scope f = do
-  res <- f Scope
-  idOf . Lam $ res
+lam argTy scope f = do
+  let scope' = pushArgToScope argTy scope
+  res <- f scope'
+  let resTy = typeOfRef res
+      lamTy = TyLam argTy resTy
+  idOf lamTy . Lam $ res
 
 -- | Given a proof of scope, a 'Ref' to an expression to bind to, and a function
 -- to construct a @let@-binding body using a \'larger\' proof of scope, construct
@@ -203,22 +233,41 @@ lam Scope f = do
 -- >     five <- lit 5
 -- >     four <- lit 4
 -- >     prod <- mul five four
--- >     letBind emptyScope prod $ \s01 ->
+-- >     letBind TyInteger emptyScope prod $ \s01 ->
 -- >          mul (ABound . bound @0 $ s01) (ABound . bound @0 $ s01)
 --
 -- @since 1.0.0
 letBind ::
   forall (n :: Natural) (m :: Natural).
+  -- | Type of the binding
+  ASGType ->
   Scope n m ->
   Ref ->
   (Scope n (m + 1) -> ASGBuilder Ref) ->
   ASGBuilder Id
-letBind Scope r f = do
-  res <- f Scope
-  idOf . Let r $ res
+letBind letTy scope r f = do
+  let scope' = pushLetToScope letTy scope
+  res <- f scope'
+  idOf letTy . Let r $ res
 
 -- Helpers
 
+pushArgToScope ::
+  forall (n :: Natural) (m :: Natural).
+  ASGType ->
+  Scope n m ->
+  Scope (n + 1) m
+pushArgToScope ty (Scope args lets) =
+  Scope (Vector.cons ty args) lets
+
+pushLetToScope ::
+  forall (n :: Natural) (m :: Natural).
+  ASGType ->
+  Scope n m ->
+  Scope n (m + 1)
+pushLetToScope ty (Scope args lets) =
+  Scope args (Vector.cons ty lets)
+
 toIdList :: ASGNode -> [Id]
 toIdList = \case
   Lit _ -> []

src/Covenant/Constant.hs

@@ -11,6 +11,7 @@ module Covenant.Constant
   ( -- * Types
     AConstant (..),
     PlutusData (..),
+    TyExpr (..),
   )
 where
 
@@ -96,7 +97,7 @@ data AConstant
   | AByteString ByteString
   | AString Text
   | APair AConstant AConstant
-  | AList (Vector AConstant)
+  | AList TyExpr (Vector AConstant)
   | AData PlutusData
   deriving stock
     ( -- | @since 1.0.0
@@ -107,6 +108,30 @@ data AConstant
       Show
     )
 
+-- | The type of Plutus expressions.
+--
+-- @since 1.0.0
+data TyExpr
+  = TyUnit
+  | TyBoolean
+  | TyInteger
+  | TyByteString
+  | TyString
+  | TyPair TyExpr TyExpr
+  | TyList TyExpr
+  | TyPlutusData
+  | TyBLS12_381G1Element
+  | TyBLS12_381G2Element
+  | TyBLS12_381PairingMLResult
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Ord,
+      -- | @since 1.0.0
+      Show
+    )
+
 -- | @since 1.0.0
 instance Arbitrary AConstant where
   {-# INLINEABLE arbitrary #-}
@@ -131,7 +156,10 @@ instance Arbitrary AConstant where
                 AByteString <$> arbitrary,
                 AString <$> arbitrary,
                 APair <$> go (size `quot` 2) <*> go (size `quot` 2),
-                AList . Vector.fromList <$> mkVec,
+                do
+                  ty <- arbitrary
+                  v <- Vector.fromList <$> mkVec
+                  pure $ AList ty v,
                 AData <$> arbitrary
               ]
       -- Note (Koz, 23/01/2025): We need this because lists must be homogenous.
@@ -154,5 +182,36 @@ instance Arbitrary AConstant where
     AByteString bs -> AByteString <$> shrink bs
     AString t -> AString <$> shrink t
     APair x y -> (APair x <$> shrink y) <> (APair <$> shrink x <*> pure y)
-    AList v -> AList <$> shrink v
+    AList ty v -> AList ty <$> shrink v
     AData dat -> AData <$> shrink dat
+
+-- | @since 1.0.0
+instance Arbitrary TyExpr where
+  {-# INLINEABLE arbitrary #-}
+  arbitrary = sized go
+    where
+      go :: Int -> Gen TyExpr
+      go size
+        | size <= 0 =
+            oneof
+              [ pure TyUnit,
+                pure TyBoolean,
+                pure TyInteger,
+                pure TyByteString,
+                pure TyString,
+                pure TyPlutusData
+              ]
+        | otherwise =
+            oneof
+              [ pure TyUnit,
+                pure TyBoolean,
+                pure TyInteger,
+                pure TyByteString,
+                pure TyString,
+                pure TyPlutusData,
+                do
+                  a <- go (size `quot` 2)
+                  b <- go (size `quot` 2)
+                  pure $ TyPair a b,
+                TyList <$> go (size - 1)
+              ]