From 29096ca754b837b8f06ae02c664d47c021d0a126 Mon Sep 17 00:00:00 2001 From: scottolsen Date: Thu, 29 Jul 2021 14:50:48 -0400 Subject: [PATCH 1/3] feat: Add an initial frontend for protocols This commit adds frontend support for two new primitives, `defprotocol` and `instance`. defprotocol defines a new protocol, a collection of zero or more interfaces. Protocols implement a form of subtyping whereby one can assert that a given type implements a number of interfaces. Types that implement a protocol are called `instances` and are added using the `instance` primitive. This commit does not yet add any logic for enforcing protocols, only the frontend code for adding them to a context. Initially, we will only support protocols in the specification of interfaces. A protocol may be used in place of any type or type variable. --- CarpHask.cabal | 1 + src/Commands.hs | 1 + src/Emit.hs | 1 + src/Forms.hs | 4 ++ src/Interfaces.hs | 6 +++ src/Obj.hs | 8 +++- src/Primitives.hs | 29 ++++++++++++- src/Protocol.hs | 101 +++++++++++++++++++++++++++++++++++++++++++++ src/StartingEnv.hs | 4 +- src/Types.hs | 8 ++++ src/TypesToC.hs | 1 + 11 files changed, 160 insertions(+), 4 deletions(-) create mode 100644 src/Protocol.hs diff --git a/CarpHask.cabal b/CarpHask.cabal index 5883451fb..bb0f27809 100644 --- a/CarpHask.cabal +++ b/CarpHask.cabal @@ -46,6 +46,7 @@ library Primitives, PrimitiveError Project, + Protocol, Qualify, Reify, RenderDocs, diff --git a/src/Commands.hs b/src/Commands.hs index 6f8238a4b..8199d8846 100644 --- a/src/Commands.hs +++ b/src/Commands.hs @@ -950,3 +950,4 @@ commandType ctx (XObj x _ _) = typeOf Ref = "ref" typeOf Deref = "deref" typeOf (Interface _ _) = "interface" + typeOf (Protocol _ _) = "protocol" diff --git a/src/Emit.hs b/src/Emit.hs index 54f4c65bf..919c9e779 100644 --- a/src/Emit.hs +++ b/src/Emit.hs @@ -173,6 +173,7 @@ toC toCMode (Binder meta root) = emitterSrc (execState (visit startingIndent roo (Match _) -> dontVisit With -> dontVisit MetaStub -> dontVisit + (Protocol _ _) -> dontVisit C c -> pure c visitStr' indent str i shouldEscape = -- This will allocate a new string every time the code runs: diff --git a/src/Forms.hs b/src/Forms.hs index f03b0d7d2..a346215fb 100644 --- a/src/Forms.hs +++ b/src/Forms.hs @@ -30,6 +30,7 @@ module Forms pattern DoPat, pattern WhilePat, pattern SetPat, + pattern ProtocolPat, ) where @@ -431,5 +432,8 @@ pattern CommandPat arity sym params <- XObj (Lst [XObj (Command arity) _ _, sym, pattern PrimitivePat :: PrimitiveFunctionType -> XObj -> [XObj] -> XObj pattern PrimitivePat arity sym params <- XObj (Lst [XObj (Primitive arity) _ _, sym, (ArrPat params)]) _ _ +pattern ProtocolPat :: XObj -> [SymPath] -> [SymPath] -> XObj +pattern ProtocolPat name interfaces instances <- XObj (Lst [XObj (Protocol interfaces instances) _ _, name]) _ _ + pattern AppPat :: XObj -> [XObj] -> [XObj] pattern AppPat f args <- (f : args) diff --git a/src/Interfaces.hs b/src/Interfaces.hs index 05395e96e..44435a187 100644 --- a/src/Interfaces.hs +++ b/src/Interfaces.hs @@ -8,6 +8,7 @@ module Interfaces retroactivelyRegisterInInterface, interfaceImplementedForTy, removeInterfaceFromImplements, + getImplementations, InterfaceError (..), ) where @@ -75,6 +76,11 @@ getFirstMatchingImplementation ctx paths ty = predicate = (== Just ty) . (xobjTy . binderXObj) global = contextGlobalEnv ctx +-- | Get the paths of interface implementations. +getImplementations :: XObj -> [SymPath] +getImplementations (XObj (Lst ((XObj (Interface _ paths) _ _):_)) _ _) = paths +getImplementations _ = [] + -- | Remove an interface from a binder's list of implemented interfaces removeInterfaceFromImplements :: SymPath -> XObj -> Context -> Context removeInterfaceFromImplements oldImplPath interface ctx = diff --git a/src/Obj.hs b/src/Obj.hs index 60b02903b..4688a15c0 100644 --- a/src/Obj.hs +++ b/src/Obj.hs @@ -128,8 +128,8 @@ instance Show Number where -- | The canonical Lisp object. data Obj = Sym SymPath SymbolMode - | MultiSym String [SymPath] -- refering to multiple functions with the same name - | InterfaceSym String -- refering to an interface. TODO: rename to InterfaceLookupSym? + | MultiSym String [SymPath] -- referring to multiple functions with the same name + | InterfaceSym String -- referring to an interface. TODO: rename to InterfaceLookupSym? | Num Ty Number | Str String | Pattern String @@ -171,6 +171,7 @@ data Obj | Deref | Interface Ty [SymPath] | C String -- C literal + | Protocol [SymPath] [SymPath] deriving (Show, Eq, Generic) instance Hashable Obj @@ -401,6 +402,7 @@ getPath (XObj (Lst (XObj (Mod _ _) _ _ : XObj (Sym path _) _ _ : _)) _ _) = path getPath (XObj (Lst (XObj (Interface _ _) _ _ : XObj (Sym path _) _ _ : _)) _ _) = path getPath (XObj (Lst (XObj (Command _) _ _ : XObj (Sym path _) _ _ : _)) _ _) = path getPath (XObj (Lst (XObj (Primitive _) _ _ : XObj (Sym path _) _ _ : _)) _ _) = path +getPath (XObj (Lst (XObj (Protocol _ _) _ _ : XObj (Sym path _) _ _ : _)) _ _) = path getPath (XObj (Sym path _) _ _) = path getPath x = SymPath [] (pretty x) @@ -486,6 +488,7 @@ pretty = visit 0 Deref -> "deref" Break -> "break" Interface _ _ -> "interface" + Protocol _ _ -> "defprotocol" With -> "with" prettyUpTo :: Int -> XObj -> String @@ -551,6 +554,7 @@ prettyUpTo lim xobj = Deref -> "" Break -> "" Interface _ _ -> "" + Protocol _ _ -> "" With -> "" prettyCaptures :: Set.Set XObj -> String diff --git a/src/Primitives.hs b/src/Primitives.hs index 675ed3afb..5601e745c 100644 --- a/src/Primitives.hs +++ b/src/Primitives.hs @@ -11,7 +11,7 @@ import Control.Monad.IO.Class (MonadIO, liftIO) import Data.Bifunctor import Data.Either (fromRight, rights) import Data.Functor ((<&>)) -import Data.List (foldl') +import Data.List (foldl', find) import Data.Maybe (fromJust, fromMaybe) import Deftype import Emit @@ -37,6 +37,7 @@ import TypePredicates import Types import Util import Web.Browser (openBrowser) +import Protocol makeNullaryPrim :: SymPath -> NullaryPrimitiveCallback -> String -> String -> (String, Binder) makeNullaryPrim p = makePrim p . NullaryPrimitive @@ -118,6 +119,32 @@ primitiveColumn x@(XObj _ i _) ctx args = where err = toEvalError ctx x (MissingInfo x) +-- | Defines a new protocol. +primitiveProtocol :: VariadicPrimitiveCallback +primitiveProtocol x ctx (s@(XObj (Sym ppath@(SymPath [] _) _) i _):paths) = + let ty = (Just (ProtocolTy [])) + ps = (map getPath paths) + pro = XObj (Lst [XObj (Protocol ps []) i (Just (ProtocolTy [])), s]) i ty + binder = toBinder pro + in if (any (not . isSym) paths) + -- TODO: Better error here. + then pure $ toEvalError ctx x (ArgumentTypeError "defprotocol" "symbols" "other" (fromJust (find (not . isSym) paths))) + else case insertTypeBinder ctx (markQualified ppath) binder of + Right ctx' -> pure (ctx', dynamicNil) + Left err -> pure $ throwErr err ctx (xobjInfo x) +primitiveProtocol x ctx y = pure $ toEvalError ctx x (ArgumentTypeError "defprotocol" "an unqualified symbol" "first" (head y)) + +-- | Make a type as an instance of a protocol. +primitiveInstance :: BinaryPrimitiveCallback +primitiveInstance x ctx (XObj (Sym protocol@(SymPath _ _) _) _ _) (XObj (Sym path _) _ _) = + case registerInstance ctx protocol path of + Left err -> pure $ throwErr err ctx (xobjInfo x) + Right ctx' -> pure (ctx', dynamicNil) +primitiveInstance x ctx (XObj (Sym _ _) _ _) y = + pure $ toEvalError ctx x (ArgumentTypeError "instance" "a symbol" "second" y) +primitiveInstance _ ctx x _ = + pure $ toEvalError ctx x (ArgumentTypeError "instance" "a symbol" "first" x) + primitiveImplements :: BinaryPrimitiveCallback primitiveImplements _ ctx x@(XObj (Sym interface@(SymPath _ _) _) _ _) (XObj (Sym path _) _ _) = do diff --git a/src/Protocol.hs b/src/Protocol.hs new file mode 100644 index 000000000..2f7614098 --- /dev/null +++ b/src/Protocol.hs @@ -0,0 +1,101 @@ +-- | Defines functions for manipulating protocols. +-- +-- Protocols are bundles of interfaces that can be used for forming type +-- hierarchies. +module Protocol + (registerInstance) +where + +import Data.Either (rights) +import Debug.Trace + +import Context +import Interfaces +import Obj +import Qualify +import Types +import Util +import Env +import Forms + +-------------------------------------------------------------------------------- +-- Data + +-- | The type of protocol errors. +data ProtocolError = + NotAType SymPath + | NotAProtocol SymPath + | NotImplemented Ty [SymPath] + +instance Show ProtocolError where + show (NotAType path) = + show path ++ "is not a type. Only types may be instances of protocols." + show (NotAProtocol path) = + show path ++ "is not a protocol." + show (NotImplemented ty paths) = + "The type " ++ show ty ++ " does not implement the following interfaces: " ++ joinWithComma (map show paths) ++ " which are required by the protocol." + +-------------------------------------------------------------------------------- +-- Protocol management functions + +-- | Add a type as a new instance of a protocol, returning an updated context. +-- +-- Types will be rejected if there are no implementations of the protocol's +-- interfaces that include the type. +registerInstance :: Context -> SymPath -> SymPath -> Either ProtocolError Context +registerInstance ctx protocol inst = + let qprotocol = markQualified protocol + in getProtocol ctx qprotocol + >>= \proto@(ProtocolPat _ interfaces _) -> getTypeFromPath inst + >>= \ty -> checkImplementations ctx interfaces ty + >> (updateProtocol proto inst ty) + >>= \newProto -> replaceLeft (NotAProtocol protocol) (replaceTypeBinder ctx qprotocol newProto) + + where updateProtocol :: XObj -> SymPath -> Ty -> Either ProtocolError Binder + updateProtocol p@(ProtocolPat name interfaces instances) i iTy = + let info = xobjInfo p + newTy = fmap (addInstance iTy) (xobjTy p) + newX = XObj (Lst [XObj (Protocol interfaces (addIfNotPresent i instances)) info newTy, name]) info newTy + in pure $ toBinder newX + updateProtocol x _ _ = Left (NotAProtocol (getPath x)) + addInstance :: Ty -> Ty -> Ty + addInstance i (ProtocolTy is) = (ProtocolTy (addIfNotPresent i is)) + addInstance _ t = t + +-------------------------------------------------------------------------------- +-- Private utilities + +-- | Given a context and path, try to retrieve an associated protocol. +getProtocol :: Context -> QualifiedPath -> Either ProtocolError XObj +getProtocol ctx protocol = + case lookupBinderInTypeEnv ctx protocol of + Right (Binder _ x@(ProtocolPat _ _ _)) -> pure x + _ -> Left $ NotAProtocol (unqualify protocol) + +-- | Just a wrapper around xobjToTy. +getTypeFromPath :: SymPath -> Either ProtocolError Ty +getTypeFromPath typath = + let x = XObj (Sym typath Symbol) Nothing Nothing + in maybe (Left (NotAType typath)) Right (xobjToTy x) + +-- | Given a list of interfaces and a type, verify that the type appears in at +-- least one implementation of each interface. +checkImplementations :: Context -> [SymPath] -> Ty -> Either ProtocolError () +checkImplementations ctx interfaces t = + let actual = traceShowId $ map binderXObj (rights (map (lookupBinderInTypeEnv ctx . markQualified) interfaces)) + impls = traceShowId $ map ((map (typeFromPath (contextGlobalEnv ctx))) . getImplementations) actual + matches = map (any ((flip isSubType) t)) impls + in if (all (==True) matches) + then pure () + else Left (NotImplemented t interfaces) + +-- | Get the type of a symbol at a given path. +-- +-- TODO: Duplicated from Concretize to prevent inclusion loops. Fix. +typeFromPath :: Env -> SymPath -> Ty +typeFromPath env p = + case searchValue env p of + Right (e, Binder _ found) + | envIsExternal e -> forceTy found + | otherwise -> error "Local bindings shouldn't be ambiguous." + _ -> error ("Couldn't find " ++ show p ++ " in env:\n" ++ prettyEnvironmentChain env) diff --git a/src/StartingEnv.hs b/src/StartingEnv.hs index bb531c4ec..161560a2b 100644 --- a/src/StartingEnv.hs +++ b/src/StartingEnv.hs @@ -311,7 +311,8 @@ dynamicModule = in [ f "defdynamic" primitiveDefdynamic "defines a new dynamic value, i.e. a value available at compile time." "(defdynamic name value)", f "meta" primitiveMeta "gets the value under `\"mykey\"` in the meta map associated with a symbol. It returns `()` if the key isn’t found." "(meta mysymbol \"mykey\")", f "definterface" primitiveDefinterface "defines a new interface (which could be a function or symbol)." "(definterface mysymbol MyType)", - f "implements" primitiveImplements "designates a function as an implementation of an interface." "(implements zero Maybe.zero)" + f "implements" primitiveImplements "designates a function as an implementation of an interface." "(implements zero Maybe.zero)", + f "instance" primitiveInstance "designates a type as an instance of a protocol." "(instance )" ] ternaries' = let f = makeTernaryPrim . spath @@ -330,6 +331,7 @@ dynamicModule = f "column" primitiveColumn "returns the column a symbol was defined on." "(column mysymbol)", f "register-type" primitiveRegisterType "registers a new type from C." "(register-type Name )", f "defmodule" primitiveDefmodule "defines a new module in which `expressions` are defined." "(defmodule MyModule )", + f "defprotocol" primitiveProtocol "defines a new protocol." "(defprotocol [interfaces])", f "register" primitiveRegister "registers a new function. This is used to define C functions and other symbols that will be available at link time." "(register name )", f "deftype" primitiveDeftype "defines a new sumtype or struct." "(deftype Name )", f "help" primitiveHelp "prints help." "(help)" diff --git a/src/Types.hs b/src/Types.hs index 8c82322fa..088ea1150 100644 --- a/src/Types.hs +++ b/src/Types.hs @@ -28,6 +28,7 @@ module Types getNameFromStructName, getStructPath, promoteNumber, + isSubType, ) where @@ -68,6 +69,7 @@ data Ty | InterfaceTy | CTy -- C literals | Universe -- the type of types of types (the type of TypeTy) + | ProtocolTy [Ty] -- the type of protocols deriving (Eq, Ord, Generic) instance Hashable Ty @@ -195,6 +197,7 @@ instance Show Ty where show DynamicTy = "Dynamic" show Universe = "Universe" show CTy = "C" + show (ProtocolTy is) = "(" ++ "Protocol " ++ joinWithSpace (map show is) ++ ")" showMaybeTy :: Maybe Ty -> String showMaybeTy (Just t) = show t @@ -375,3 +378,8 @@ promoteNumber DoubleTy _ = DoubleTy promoteNumber _ DoubleTy = DoubleTy promoteNumber a b = error ("promoteNumber called with non-numbers: " ++ show a ++ ", " ++ show b) + +-- | Checks if one type contains another. +isSubType :: Ty -> Ty -> Bool +isSubType (FuncTy args ret _) t = (any (==t) args) || ret == t +isSubType t t' = t == t' diff --git a/src/TypesToC.hs b/src/TypesToC.hs index 6fc4778a2..f8fb2d500 100644 --- a/src/TypesToC.hs +++ b/src/TypesToC.hs @@ -55,4 +55,5 @@ tyToCManglePtr _ ty = f ty f (PointerTy _) = err "pointers" f (RefTy _ _) = err "references" f CTy = "c_code" -- Literal C; we shouldn't emit anything. + f (ProtocolTy _) = err "protocols" err s = error ("Can't emit the type of " ++ s ++ ".") From 32dbe2feeae8cdf0142c8087630f4c0f719ee178 Mon Sep 17 00:00:00 2001 From: scottolsen Date: Thu, 29 Jul 2021 18:57:38 -0400 Subject: [PATCH 2/3] feat: respect protocols in the type system This commit finalizes an initial implementation of protocols by updating the type system to treat them as instances of constrained polymorphism (that is, like var types but more restrictive). Protocols are a form of type constraint whereby only types that implement a set of interfaces may be used in the place of a protocol. Here's the gist of how they work: To define a protocol, a user enters `(defprotocol [interfaces...])`. `defprotocol` adds a fresh protocol to the type environment, inhabited by no types. Users then register types with the protocol using `(instance )`. The type will only be registered if it appears in at least one position of the signatures of the protocol's interface's implementations. That is, if there is no existing implementation of all for the type, it cannot be added to the protocol. Users can then reference protocols in type signatures by prefixing their names with `!`. For example, `(sig foo (Fn [!Stringable] String))`. When we type check protocols, we update the state of types based on the current state of the type environment (since a protocol's members may have changed). If the type being passed in the place of a protocol is a member of the protocol, it successfully type checks. Otherwise, it fails to type check. Protocols can also be used for arbitrary "tagging" or "subtyping" over types by defining empty protocols. If a user wants to simply specify a type union, they can call: `(defprotocol Empty)` which will define a protocol that has no interfaces. Any type may be added to this protocol. --- src/Concretize.hs | 7 ++-- src/Constraints.hs | 12 +++++++ src/Emit.hs | 1 + src/InitialTypes.hs | 5 +-- src/Interfaces.hs | 9 ++--- src/Obj.hs | 13 +++++++- src/Primitives.hs | 11 ++++--- src/Protocol.hs | 77 +++++++++++++++++++++++++++++++++++-------- src/TypePredicates.hs | 1 + src/Types.hs | 10 ++++-- src/TypesToC.hs | 2 +- 11 files changed, 114 insertions(+), 34 deletions(-) diff --git a/src/Concretize.hs b/src/Concretize.hs index 146209293..5e99c14b9 100644 --- a/src/Concretize.hs +++ b/src/Concretize.hs @@ -27,6 +27,7 @@ import TypesToC import Util import Validate import Prelude hiding (lookup) +import Protocol data Level = Toplevel | Inside @@ -337,13 +338,13 @@ concretizeXObj allowAmbiguityRoot typeEnv rootEnv visitedDefinitions root = visitInterfaceSym allowAmbig env xobj@(XObj (InterfaceSym name) i t) = case getTypeBinder typeEnv name of Right (Binder _ (XObj (Lst [XObj (Interface _ interfacePaths) _ _, _]) _ _)) -> - let Just actualType = t + let Just actualType = fmap (updateProtocols typeEnv) t tys = map (typeFromPath env) interfacePaths tysToPathsDict = zip tys interfacePaths in case filter (matchingSignature actualType) tysToPathsDict of [] -> pure $ --(trace ("No matching signatures for interface lookup of " ++ name ++ " of type " ++ show actualType ++ " " ++ prettyInfoFromXObj xobj ++ ", options are:\n" ++ joinLines (map show tysToPathsDict))) $ - if allowAmbig + if allowAmbig || containsProtocol actualType then Right xobj -- No exact match of types else Left (NoMatchingSignature xobj name actualType tysToPathsDict) [(theType, singlePath)] -> @@ -685,7 +686,7 @@ modeFromPath env p = concretizeDefinition :: Bool -> TypeEnv -> Env -> [SymPath] -> XObj -> Ty -> Either TypeError (XObj, [XObj]) concretizeDefinition allowAmbiguity typeEnv globalEnv visitedDefinitions definition concreteType = let SymPath pathStrings name = getPath definition - Just polyType = xobjTy definition + Just polyType = fmap (updateProtocols typeEnv) (xobjTy definition) suffix = polymorphicSuffix polyType concreteType newPath = SymPath pathStrings (name ++ suffix) in case definition of diff --git a/src/Constraints.hs b/src/Constraints.hs index 851b12347..ea4517f78 100644 --- a/src/Constraints.hs +++ b/src/Constraints.hs @@ -176,6 +176,18 @@ solveOneInternal mappings constraint = in case solveOneInternal mappings (Constraint v (RefTy b ltB) i1 i2 ctx ord) of Left err -> Left err Right ok -> foldM (\m (aa, bb) -> solveOneInternal m (Constraint aa bb i1 i2 ctx ord)) ok (zip args [b, ltB]) + Constraint (ProtocolTy path _) (ProtocolTy path' _) _ _ _ _ -> + if path == path' + then Right mappings + else Left (UnificationFailure constraint mappings) + Constraint t (ProtocolTy (SymPath [] key) ts) _ _ _ _ -> + if t `elem` ts + then Right (Map.insert key t mappings) + else Left (UnificationFailure constraint mappings) + Constraint (ProtocolTy (SymPath [] key) ts) t _ _ _ _ -> + if t `elem` ts + then Right (Map.insert key t mappings) + else Left (UnificationFailure constraint mappings) -- Else Constraint aTy bTy _ _ _ _ -> if aTy == bTy diff --git a/src/Emit.hs b/src/Emit.hs index 919c9e779..0f2a3997b 100644 --- a/src/Emit.hs +++ b/src/Emit.hs @@ -926,6 +926,7 @@ toDeclaration (Binder meta xobj@(XObj (Lst xobjs) _ ty)) = "" XObj (Primitive _) _ _ : _ -> "" + XObj (Protocol _ _) _ _ : _ -> "" _ -> error ("Internal compiler error: Can't emit other kinds of definitions: " ++ show xobj) toDeclaration _ = error "Missing case." diff --git a/src/InitialTypes.hs b/src/InitialTypes.hs index 5506cfd55..3c0f79af7 100644 --- a/src/InitialTypes.hs +++ b/src/InitialTypes.hs @@ -9,6 +9,7 @@ import qualified Set import TypeError import Types import Util +import Protocol -- | Create a fresh type variable (eg. 'VarTy t0', 'VarTy t1', etc...) genVarTyWithPrefix :: String -> State Integer Ty @@ -138,7 +139,7 @@ initialTypes typeEnv rootEnv root = evalState (visit rootEnv root) 0 -- Don't rename internal symbols like parameters etc! Just theType | envIsExternal foundEnv -> do - renamed <- renameVarTys theType + renamed <- renameVarTys (updateProtocols typeEnv theType) pure (Right (xobj {xobjTy = Just renamed})) | otherwise -> pure (Right (xobj {xobjTy = Just theType})) Nothing -> pure (Left (SymbolMissingType xobj foundEnv)) @@ -153,7 +154,7 @@ initialTypes typeEnv rootEnv root = evalState (visit rootEnv root) 0 visitInterfaceSym _ xobj@(XObj (InterfaceSym name) _ _) = do freshTy <- case getTypeBinder typeEnv name of - Right (Binder _ (XObj (Lst [XObj (Interface interfaceSignature _) _ _, _]) _ _)) -> renameVarTys interfaceSignature + Right (Binder _ (XObj (Lst [XObj (Interface interfaceSignature _) _ _, _]) _ _)) -> (renameVarTys (updateProtocols typeEnv interfaceSignature)) Right (Binder _ x) -> error ("A non-interface named '" ++ name ++ "' was found in the type environment: " ++ pretty x) Left _ -> genVarTy pure (Right xobj {xobjTy = Just freshTy}) diff --git a/src/Interfaces.hs b/src/Interfaces.hs index 44435a187..2cfa29b2d 100644 --- a/src/Interfaces.hs +++ b/src/Interfaces.hs @@ -8,7 +8,6 @@ module Interfaces retroactivelyRegisterInInterface, interfaceImplementedForTy, removeInterfaceFromImplements, - getImplementations, InterfaceError (..), ) where @@ -24,6 +23,7 @@ import Obj import qualified Qualify import Types import Util +import Protocol data InterfaceError = KindMismatch SymPath Ty Ty @@ -76,11 +76,6 @@ getFirstMatchingImplementation ctx paths ty = predicate = (== Just ty) . (xobjTy . binderXObj) global = contextGlobalEnv ctx --- | Get the paths of interface implementations. -getImplementations :: XObj -> [SymPath] -getImplementations (XObj (Lst ((XObj (Interface _ paths) _ _):_)) _ _) = paths -getImplementations _ = [] - -- | Remove an interface from a binder's list of implemented interfaces removeInterfaceFromImplements :: SymPath -> XObj -> Context -> Context removeInterfaceFromImplements oldImplPath interface ctx = @@ -105,7 +100,7 @@ registerInInterfaceIfNeeded ctx implementation interface definitionSignature = case interface of Binder _ (XObj (Lst [inter@(XObj (Interface interfaceSignature paths) ii it), isym]) i t) -> if checkKinds interfaceSignature definitionSignature - then case solve [Constraint interfaceSignature definitionSignature inter inter inter OrdInterfaceImpl] of + then case solve [Constraint (resolveProtocols ctx interfaceSignature) definitionSignature inter inter inter OrdInterfaceImpl] of Left _ -> (Right ctx, Just (TypeMismatch implPath definitionSignature interfaceSignature)) Right _ -> case getFirstMatchingImplementation ctx paths definitionSignature of Nothing -> (updatedCtx, Nothing) diff --git a/src/Obj.hs b/src/Obj.hs index 4688a15c0..8faf1bb8b 100644 --- a/src/Obj.hs +++ b/src/Obj.hs @@ -817,8 +817,12 @@ xobjToTy (XObj (Sym (SymPath _ "Pattern") _) _ _) = Just PatternTy xobjToTy (XObj (Sym (SymPath _ "Char") _) _ _) = Just CharTy xobjToTy (XObj (Sym (SymPath _ "Bool") _) _ _) = Just BoolTy xobjToTy (XObj (Sym (SymPath _ "Static") _) _ _) = Just StaticLifetimeTy -xobjToTy (XObj (Sym spath@(SymPath _ s@(firstLetter : _)) _) _ _) +xobjToTy (XObj (Sym spath@(SymPath _ s@(firstLetter : rest)) _) _ _) | isLower firstLetter = Just (VarTy s) + | firstLetter == '!' = + if (not (null rest)) + then Just (ProtocolTy (SymPath [] rest) []) + else Nothing | otherwise = Just (StructTy (ConcreteNameTy spath) []) xobjToTy (XObj (Lst [XObj (Sym (SymPath _ "Ptr") _) _ _, innerTy]) _ _) = do @@ -894,6 +898,13 @@ polymorphicSuffix signature actualType = else do put (a : visitedTypeVariables) -- now it's visited pure [tyToC b] + (p@(ProtocolTy _ _), t) -> do + visitedTypeVariables <- get + if p `elem` visitedTypeVariables + then pure [] + else do + put (p : visitedTypeVariables) -- now it's visited + pure [tyToC t] (FuncTy argTysA retTyA _, FuncTy argTysB retTyB _) -> do visitedArgs <- fmap concat (zipWithM visit argTysA argTysB) visitedRets <- visit retTyA retTyB diff --git a/src/Primitives.hs b/src/Primitives.hs index 5601e745c..f4c59ef57 100644 --- a/src/Primitives.hs +++ b/src/Primitives.hs @@ -122,9 +122,9 @@ primitiveColumn x@(XObj _ i _) ctx args = -- | Defines a new protocol. primitiveProtocol :: VariadicPrimitiveCallback primitiveProtocol x ctx (s@(XObj (Sym ppath@(SymPath [] _) _) i _):paths) = - let ty = (Just (ProtocolTy [])) + let ty = (Just (ProtocolTy ppath [])) ps = (map getPath paths) - pro = XObj (Lst [XObj (Protocol ps []) i (Just (ProtocolTy [])), s]) i ty + pro = XObj (Lst [XObj (Protocol ps []) i ty, s]) i ty binder = toBinder pro in if (any (not . isSym) paths) -- TODO: Better error here. @@ -490,15 +490,16 @@ primitiveDefinterface xobj ctx nameXObj@(XObj (Sym path@(SymPath [] name) _) _ _ invalidType = evalError ctx ("Invalid type for interface `" ++ name ++ "`: " ++ pretty ty) (xobjInfo ty) validType t = either (const defInterface) updateInterface (lookupBinderInTypeEnv ctx path) where - defInterface = - let interface = defineInterface name t [] (xobjInfo nameXObj) + withProtocols = resolveProtocols ctx t + defInterface = + let interface = defineInterface name withProtocols [] (xobjInfo nameXObj) binder = toBinder interface Right ctx' = insertTypeBinder ctx (markQualified (SymPath [] name)) binder Right newCtx = retroactivelyRegisterInInterface ctx' binder in (newCtx, dynamicNil) updateInterface binder = case binder of Binder _ (XObj (Lst (XObj (Interface foundType _) _ _ : _)) _ _) -> - if foundType == t + if protocolEq foundType withProtocols then (ctx, dynamicNil) else evalError diff --git a/src/Protocol.hs b/src/Protocol.hs index 2f7614098..f5106ba3f 100644 --- a/src/Protocol.hs +++ b/src/Protocol.hs @@ -2,15 +2,26 @@ -- -- Protocols are bundles of interfaces that can be used for forming type -- hierarchies. +-- +-- Protocols have global state in the type environment. The functions +-- resolveProtocols and updateProtocols allow callees to fetch the latest +-- protocol state to update the protocol types associated with functions. +-- +-- Protocols leverage the same polymorphism resolution as type variables, but +-- permissible substitutions are given by their members. module Protocol - (registerInstance) + (registerInstance + ,resolveProtocols + ,protocolEq + ,updateProtocols + ,containsProtocol + ,isProtocol) where +import Data.Maybe (fromJust) import Data.Either (rights) -import Debug.Trace import Context -import Interfaces import Obj import Qualify import Types @@ -59,35 +70,61 @@ registerInstance ctx protocol inst = in pure $ toBinder newX updateProtocol x _ _ = Left (NotAProtocol (getPath x)) addInstance :: Ty -> Ty -> Ty - addInstance i (ProtocolTy is) = (ProtocolTy (addIfNotPresent i is)) - addInstance _ t = t + addInstance i (ProtocolTy n is) = (ProtocolTy n (addIfNotPresent i is)) + addInstance _ t = t + +-- | Given a designation of a protocol, resolve it to the protocol's current +-- memberships in the given context. +resolveProtocols :: Context -> Ty -> Ty +resolveProtocols ctx (FuncTy args ret lt) = (FuncTy (map (resolveProtocols ctx) args) (resolveProtocols ctx ret) lt) +resolveProtocols ctx p@(ProtocolTy path _) = + case lookupBinderInTypeEnv ctx (markQualified path) of + Right p' -> fromJust (xobjTy (binderXObj p')) + Left _ -> p +resolveProtocols _ t = t + +-- | Same as resolveProtocols, but operates on a type environment. +updateProtocols :: TypeEnv -> Ty -> Ty +updateProtocols tenv (FuncTy args ret lt) = (FuncTy (map (updateProtocols tenv) args) (updateProtocols tenv ret) lt) +updateProtocols tenv p@(ProtocolTy path _) = + case findTypeBinder tenv path of + Right p' -> fromJust (xobjTy (binderXObj p')) + Left _ -> p +updateProtocols _ t = t + +-- | Check that two types are equal, ignoring differences in protocol membership. +protocolEq :: Ty -> Ty -> Bool +protocolEq (FuncTy args ret lt) (FuncTy args' ret' lt') = + (foldl (&&) True (zipWith protocolEq args args')) && protocolEq ret ret' && lt == lt' +protocolEq (ProtocolTy name _) (ProtocolTy name' _) = name == name' +protocolEq t t' = t == t' -------------------------------------------------------------------------------- -- Private utilities -- | Given a context and path, try to retrieve an associated protocol. -getProtocol :: Context -> QualifiedPath -> Either ProtocolError XObj -getProtocol ctx protocol = - case lookupBinderInTypeEnv ctx protocol of +getProtocol :: Context -> QualifiedPath -> Either ProtocolError XObj +getProtocol ctx protocol = + case lookupBinderInTypeEnv ctx protocol of Right (Binder _ x@(ProtocolPat _ _ _)) -> pure x - _ -> Left $ NotAProtocol (unqualify protocol) + _ -> Left $ NotAProtocol (unqualify protocol) -- | Just a wrapper around xobjToTy. getTypeFromPath :: SymPath -> Either ProtocolError Ty getTypeFromPath typath = let x = XObj (Sym typath Symbol) Nothing Nothing in maybe (Left (NotAType typath)) Right (xobjToTy x) - + -- | Given a list of interfaces and a type, verify that the type appears in at -- least one implementation of each interface. checkImplementations :: Context -> [SymPath] -> Ty -> Either ProtocolError () checkImplementations ctx interfaces t = - let actual = traceShowId $ map binderXObj (rights (map (lookupBinderInTypeEnv ctx . markQualified) interfaces)) - impls = traceShowId $ map ((map (typeFromPath (contextGlobalEnv ctx))) . getImplementations) actual + let actual = map binderXObj (rights (map (lookupBinderInTypeEnv ctx . markQualified) interfaces)) + impls = map ((map (typeFromPath (contextGlobalEnv ctx))) . getImplementations) actual matches = map (any ((flip isSubType) t)) impls in if (all (==True) matches) then pure () - else Left (NotImplemented t interfaces) + else Left (NotImplemented t (map snd (filter (\(tf, _) -> (not tf)) (zip matches interfaces)))) -- | Get the type of a symbol at a given path. -- @@ -99,3 +136,17 @@ typeFromPath env p = | envIsExternal e -> forceTy found | otherwise -> error "Local bindings shouldn't be ambiguous." _ -> error ("Couldn't find " ++ show p ++ " in env:\n" ++ prettyEnvironmentChain env) + +-- | Get the paths of interface implementations. +getImplementations :: XObj -> [SymPath] +getImplementations (XObj (Lst ((XObj (Interface _ paths) _ _):_)) _ _) = paths +getImplementations _ = [] + +containsProtocol :: Ty -> Bool +containsProtocol (FuncTy args ret _) = (any containsProtocol args) || containsProtocol ret +containsProtocol (ProtocolTy _ _) = True +containsProtocol _ = False + +isProtocol :: Ty -> Bool +isProtocol (ProtocolTy _ _) = True +isProtocol _ = False diff --git a/src/TypePredicates.hs b/src/TypePredicates.hs index 4cde4feaa..ac97d9dda 100644 --- a/src/TypePredicates.hs +++ b/src/TypePredicates.hs @@ -4,6 +4,7 @@ import Types isTypeGeneric :: Ty -> Bool isTypeGeneric (VarTy _) = True +isTypeGeneric (ProtocolTy _ _) = True isTypeGeneric (FuncTy argTys retTy _) = any isTypeGeneric argTys || isTypeGeneric retTy isTypeGeneric (StructTy n tyArgs) = isTypeGeneric n || any isTypeGeneric tyArgs isTypeGeneric (PointerTy p) = isTypeGeneric p diff --git a/src/Types.hs b/src/Types.hs index 088ea1150..43daa28ba 100644 --- a/src/Types.hs +++ b/src/Types.hs @@ -69,7 +69,7 @@ data Ty | InterfaceTy | CTy -- C literals | Universe -- the type of types of types (the type of TypeTy) - | ProtocolTy [Ty] -- the type of protocols + | ProtocolTy SymPath [Ty] -- the type of protocols deriving (Eq, Ord, Generic) instance Hashable Ty @@ -197,7 +197,8 @@ instance Show Ty where show DynamicTy = "Dynamic" show Universe = "Universe" show CTy = "C" - show (ProtocolTy is) = "(" ++ "Protocol " ++ joinWithSpace (map show is) ++ ")" + show (ProtocolTy s []) = "(" ++ "Protocol " ++ show s ++ ")" + show (ProtocolTy s is) = "(" ++ "Protocol " ++ show s ++ ": " ++ joinWithComma (map show is) ++ ")" showMaybeTy :: Maybe Ty -> String showMaybeTy (Just t) = show t @@ -245,6 +246,7 @@ unifySignatures at ct = Map.fromList (unify at ct) unify :: Ty -> Ty -> [(String, Ty)] unify (VarTy _) (VarTy _) = [] -- if a == b then [] else error ("Can't unify " ++ show a ++ " with " ++ show b) unify (VarTy a) value = [(a, value)] + unify (ProtocolTy (SymPath [] name) ts) t = if t `elem` ts then [(name,t)] else [] unify (StructTy v'@(VarTy _) aArgs) (StructTy n bArgs) = unify v' n ++ concat (zipWith unify aArgs bArgs) unify (StructTy a@(ConcreteNameTy _) aArgs) (StructTy b bArgs) | a == b = concat (zipWith unify aArgs bArgs) @@ -281,6 +283,9 @@ areUnifiable (StructTy (VarTy _) aArgs) (FuncTy bArgs _ _) areUnifiable (StructTy (VarTy _) args) (RefTy _ _) | length args == 2 = True | otherwise = False +areUnifiable (ProtocolTy n _) (ProtocolTy n' _) = n == n' +areUnifiable t (ProtocolTy _ ts) = t `elem` ts +areUnifiable (ProtocolTy _ ts) t = t `elem` ts areUnifiable (StructTy _ _) _ = False areUnifiable (PointerTy a) (PointerTy b) = areUnifiable a b areUnifiable (PointerTy _) _ = False @@ -316,6 +321,7 @@ replaceTyVars :: TypeMappings -> Ty -> Ty replaceTyVars mappings t = case t of (VarTy key) -> fromMaybe t (Map.lookup key mappings) + (ProtocolTy (SymPath [] key) _) -> fromMaybe t (Map.lookup key mappings) (FuncTy argTys retTy lt) -> FuncTy (map (replaceTyVars mappings) argTys) (replaceTyVars mappings retTy) (replaceTyVars mappings lt) (StructTy name tyArgs) -> case replaceTyVars mappings name of diff --git a/src/TypesToC.hs b/src/TypesToC.hs index f8fb2d500..df53e7ece 100644 --- a/src/TypesToC.hs +++ b/src/TypesToC.hs @@ -55,5 +55,5 @@ tyToCManglePtr _ ty = f ty f (PointerTy _) = err "pointers" f (RefTy _ _) = err "references" f CTy = "c_code" -- Literal C; we shouldn't emit anything. - f (ProtocolTy _) = err "protocols" + f (ProtocolTy _ _) = err "protocols" err s = error ("Can't emit the type of " ++ s ++ ".") From 13777addb11d75f1cbf449a31e30e84cb7c4109b Mon Sep 17 00:00:00 2001 From: scottolsen Date: Thu, 29 Jul 2021 19:14:39 -0400 Subject: [PATCH 3/3] feat: print interfaces in protocol info strings --- src/Primitives.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Primitives.hs b/src/Primitives.hs index f4c59ef57..a3ce1b8dc 100644 --- a/src/Primitives.hs +++ b/src/Primitives.hs @@ -38,6 +38,7 @@ import Types import Util import Web.Browser (openBrowser) import Protocol +import Forms makeNullaryPrim :: SymPath -> NullaryPrimitiveCallback -> String -> String -> (String, Binder) makeNullaryPrim p = makePrim p . NullaryPrimitive @@ -308,6 +309,7 @@ primitiveInfo _ ctx target@(XObj (Sym path@(SymPath _ name) _) _ _) = let found = lookupBinderInTypeEnv ctx path _ <- printIfFound found _ <- printInterfaceImplementationsOrAll found otherBindings + _ <- printProtocolInterfaces found either (const (notFound ctx target path)) (const ok) (found <> fmap head otherBindings) where otherBindings = @@ -323,6 +325,10 @@ primitiveInfo _ ctx target@(XObj (Sym path@(SymPath _ name) _) _ _) = where ok :: IO (Context, Either EvalError XObj) ok = pure (ctx, dynamicNil) + printProtocolInterfaces :: Either ContextError Binder -> IO () + printProtocolInterfaces (Right (Binder _ (ProtocolPat _ interfaces _))) = + putStrLn $ " Required Definitions: " ++ joinWithComma (map show interfaces) + printProtocolInterfaces _ = pure () printInterfaceImplementationsOrAll :: Either ContextError Binder -> Either ContextError [Binder] -> IO () printInterfaceImplementationsOrAll interface impls = either