From a4a2a08f7ecb08f764e33f6dcb7dc50d82b0c69d Mon Sep 17 00:00:00 2001 From: Adam Paszke Date: Fri, 1 Oct 2021 11:52:39 +0000 Subject: [PATCH] Add explicit interface methods It is often useful to define type -> value mappings, and the standard way to do that is through interfaces (type classes). However, because all methods so far had implicit type parameters, any attempt to associate e.g. an integer with a type was difficult: without explicit type annotations it often ended up being ambiguous. This patch adds a new keyword `explicit` that makes it possible to require that all types parameterizing a type class are to be taken as explicit arguments of a given method. This lets us remove the awkward `TypeVehicle` abstraction from prelude and in the future should make it possible to define associated types. For example, a `Manifold` interface could have a method declared as `explicit TangentSpace : Type`, which would later make it possible to mention e.g. `TangentSpace MyDataType` in types. --- lib/prelude.dx | 18 +++++------------- src/lib/Builder.hs | 13 +++++++------ src/lib/Inference.hs | 8 ++++---- src/lib/PPrint.hs | 8 ++++++-- src/lib/Parser.hs | 8 ++++++-- src/lib/SourceRename.hs | 3 +++ src/lib/Syntax.hs | 10 ++++++++-- 7 files changed, 39 insertions(+), 29 deletions(-) diff --git a/lib/prelude.dx b/lib/prelude.dx index af4f7155c..eaee7d300 100644 --- a/lib/prelude.dx +++ b/lib/prelude.dx @@ -676,38 +676,30 @@ def castPtr (ptr: Ptr a) : Ptr b = (MkPtr rawPtr) = ptr MkPtr rawPtr --- Is there a better way to select the right instance for `storageSize`?? -data TypeVehicle a = MkTypeVehicle -def typeVehicle (a:Type) : TypeVehicle a = MkTypeVehicle - interface Storable a store : Ptr a -> a -> {IO} Unit load : Ptr a -> {IO} a - storageSize_ : TypeVehicle a -> Int - -def storageSize (a:Type) -> (d:Storable a) ?=> : Int = - tv : TypeVehicle a = MkTypeVehicle - storageSize_ tv + explicit storageSize : Int instance Storable Word8 store = \(MkPtr ptr) x. %ptrStore ptr x load = \(MkPtr ptr) . %ptrLoad ptr - storageSize_ = const 1 + storageSize = 1 instance Storable Int32 store = \(MkPtr ptr) x. %ptrStore (internalCast %Int32Ptr ptr) x load = \(MkPtr ptr) . %ptrLoad (internalCast %Int32Ptr ptr) - storageSize_ = const 4 + storageSize = 4 instance Storable Float32 store = \(MkPtr ptr) x. %ptrStore (internalCast %Float32Ptr ptr) x load = \(MkPtr ptr) . %ptrLoad (internalCast %Float32Ptr ptr) - storageSize_ = const 4 + storageSize = 4 instance Storable (Ptr a) store = \(MkPtr ptr) (MkPtr x). %ptrStore (internalCast %PtrPtr ptr) x load = \(MkPtr ptr) . MkPtr $ %ptrLoad (internalCast %PtrPtr ptr) - storageSize_ = const 8 -- TODO: something more portable? + storageSize = 8 -- TODO: something more portable? -- TODO: Storable instances for other types diff --git a/src/lib/Builder.hs b/src/lib/Builder.hs index 56df2e4cf..328c9d9c1 100644 --- a/src/lib/Builder.hs +++ b/src/lib/Builder.hs @@ -261,15 +261,16 @@ emitSuperclass dataDef idx = do getter <- makeSuperclassGetter dataDef idx emitBinding $ SuperclassName dataDef idx getter -emitMethodType :: MonadBuilder m => ClassDefName -> Int -> m Name -emitMethodType classDef idx = do - getter <- makeMethodGetter classDef idx +emitMethodType :: MonadBuilder m => MethodKind -> ClassDefName -> Int -> m Name +emitMethodType kind classDef idx = do + getter <- makeMethodGetter kind classDef idx emitBinding $ MethodName classDef idx getter -makeMethodGetter :: MonadBuilder m => ClassDefName -> Int -> m Atom -makeMethodGetter classDefName methodIdx = do +makeMethodGetter :: MonadBuilder m => MethodKind -> ClassDefName -> Int -> m Atom +makeMethodGetter kind classDefName methodIdx = do ClassDef def@(_, DataDef _ paramBs _) _ <- getClassDef classDefName - buildImplicitNaryLam paramBs \params -> do + let arrow = case kind of ImplicitMethod -> ImplicitArrow; ExplicitMethod -> PureArrow + buildNaryLam arrow paramBs \params -> do buildLam (Bind ("d":> TypeCon def params)) ClassArrow \dict -> do return $ getProjection [methodIdx] $ getProjection [1, 0] dict diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs index 3f9bc8b14..c6d09bd9a 100644 --- a/src/lib/Inference.hs +++ b/src/lib/Inference.hs @@ -367,8 +367,8 @@ inferUDecl (UInterface paramBs superclasses methodTys className methodNames) = d paramBs superclasses methodTys className' <- withNameHint className $ emitClassDef classDef mapM_ (emitSuperclass className') [0..(length superclasses - 1)] - methodNames' <- forM (enumerate (toList methodNames)) \(i, name) -> - withNameHint name $ emitMethodType className' i + methodNames' <- forM (enumerate $ zip (toList methodNames) (fmap fst methodTys)) \(i, (name, k)) -> do + withNameHint name $ emitMethodType k className' i return $ className @> Rename className' <> newEnv methodNames (map Rename methodNames') inferUDecl (UInstance argBinders ~(UInternalVar className) params methods maybeName) = do @@ -391,11 +391,11 @@ inferDataDef (UDataDef (tyConName, paramBs) dataCons) = return $ DataDef tyConName paramBs' dataCons' inferInterfaceDataDef :: SourceName -> [SourceName] -> Nest UAnnBinder - -> [UType] -> [UType] -> UInferM ClassDef + -> [UType] -> [UMethodType] -> UInferM ClassDef inferInterfaceDataDef className methodNames paramBs superclasses methods = do dictDef <- withNestedBinders paramBs \paramBs' -> do superclasses' <- mapM checkUType superclasses - methods' <- mapM checkUType methods + methods' <- mapM checkUType $ snd <$> methods let dictContents = PairTy (ProdTy superclasses') (ProdTy methods') return $ DataDef className paramBs' [DataConDef ("Mk"<>className) (Nest (Ignore dictContents) Empty)] diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs index f939740db..35f993007 100644 --- a/src/lib/PPrint.hs +++ b/src/lib/PPrint.hs @@ -686,15 +686,19 @@ instance Pretty UDecl where "data" <+> p bTyCon <+> p bParams <+> "where" <> nest 2 (hardline <> prettyLines (zip (toList bDataCons) dataCons)) pretty (UInterface params superclasses methodTys interfaceName methodNames) = - let methods = [UAnnBinder b ty | (b, ty) <- zip (toList methodNames) methodTys] + let methods = [p k <+> p (UAnnBinder b ty) | (b, (k, ty)) <- zip (toList methodNames) methodTys] in "interface" <+> p params <+> p superclasses <+> p interfaceName - <> hardline <> prettyLines methods + <> hardline <> foldMap (<>hardline) methods pretty (UInstance bs className params methods Nothing) = "instance" <+> p bs <+> p className <+> p params <+> hardline <> prettyLines methods pretty (UInstance bs className params methods (Just v)) = "named-instance" <+> p v <+> ":" <+> p bs <+> p className <+> p params <> hardline <> prettyLines methods +instance Pretty MethodKind where + pretty ImplicitMethod = "" + pretty ExplicitMethod = "explicit" + instance Pretty UPatAnnArrow where pretty (UPatAnnArrow b arr) = p b <> ":" <> p arr diff --git a/src/lib/Parser.hs b/src/lib/Parser.hs index bb71e20d6..00bc39f90 100644 --- a/src/lib/Parser.hs +++ b/src/lib/Parser.hs @@ -238,9 +238,10 @@ interfaceDef = do superclasses <- superclassConstraints (tyConName, tyConParams) <- tyConDef (methodNames, methodTys) <- unzip <$> onePerLine do + k <- (keyWord ExplicitKW $> ExplicitMethod) <|> pure ImplicitMethod v <- anyName ty <- annot uType - return (fromString v, ty) + return (fromString v, (k, ty)) let methodNames' = toNest methodNames let tyConParams' = tyConParams return $ UInterface tyConParams' superclasses methodTys (fromString tyConName) methodNames' @@ -895,6 +896,7 @@ data KeyWord = DefKW | ForKW | For_KW | RofKW | Rof_KW | CaseKW | OfKW | ReadKW | WriteKW | StateKW | DataKW | InterfaceKW | InstanceKW | WhereKW | IfKW | ThenKW | ElseKW | DoKW | ExceptKW | IOKW | ViewKW | ImportKW | NamedInstanceKW + | ExplicitKW upperName :: Lexer SourceName upperName = label "upper-case name" $ lexeme $ @@ -943,11 +945,13 @@ keyWord kw = lexeme $ try $ string s >> notFollowedBy nameTailChar DoKW -> "do" ViewKW -> "view" ImportKW -> "import" + ExplicitKW -> "explicit" keyWordStrs :: [String] keyWordStrs = ["def", "for", "for_", "rof", "rof_", "case", "of", "llam", "Read", "Write", "Accum", "Except", "IO", "data", "interface", - "instance", "named-instance", "where", "if", "then", "else", "do", "view", "import"] + "instance", "named-instance", "where", "if", "then", "else", + "do", "view", "import", "explicit"] fieldLabel :: Lexer Label fieldLabel = label "field label" $ lexeme $ diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index bc7aaa95a..27f2b05af 100644 --- a/src/lib/SourceRename.hs +++ b/src/lib/SourceRename.hs @@ -188,6 +188,9 @@ instance SourceRenamableB UDecl where instanceName' <- mapM sourceRenameB instanceName return $ UInstance conditions' className' params' methodDefs' instanceName' +instance SourceRenamableE MethodKind where + sourceRenameE = return + sourceRenameUBinderNest :: Renamer m => (Name -> SourceNameDef) -> Nest UBinder -> WithEnv RenameEnv m (Nest UBinder) sourceRenameUBinderNest _ Empty = return Empty diff --git a/src/lib/Syntax.hs b/src/lib/Syntax.hs index f4bebba43..0d84f69d2 100644 --- a/src/lib/Syntax.hs +++ b/src/lib/Syntax.hs @@ -42,7 +42,7 @@ module Syntax ( monMapSingle, monMapLookup, Direction (..), Limit (..), SourceName, SourceMap (..), UExpr, UExpr' (..), UType, UPatAnn (..), UAnnBinder (..), UVar (..), UBinder (..), UMethodDef (..), - UMethodTypeDef, UPatAnnArrow (..), UVars, + MethodKind (..), UMethodType, UMethodTypeDef, UPatAnnArrow (..), UVars, UPat, UPat' (..), SourceUModule (..), SourceNameDef (..), sourceNameDefName, UModule (..), UDecl (..), UDataDef (..), UArrow, arrowEff, UEffect, UEffectRow, UEffArrow, @@ -274,6 +274,9 @@ data UDataDef = UDataDef [(SourceName, Nest UAnnBinder)] -- data constructor types deriving (Show, Generic) +data MethodKind = ExplicitMethod | ImplicitMethod + deriving (Show, Generic) +type UMethodType = (MethodKind, UType) -- NOTE: Pairs are functors in second component data UDecl = ULet LetAnn UPatAnn UExpr | UDataDefDecl @@ -283,7 +286,7 @@ data UDecl = | UInterface (Nest UAnnBinder) -- parameter binders [UType] -- superclasses - [UType] -- method types + [UMethodType] -- method types UBinder -- class name (Nest UBinder) -- method names | UInstance @@ -827,6 +830,9 @@ instance HasUVars UDecl where freeUVars (UInstance bs className params methods _) = freeUVars $ Abs bs ((className, params), methods) +instance HasUVars MethodKind where + freeUVars _ = mempty + instance (BindsUVars b1, HasUVars b1, HasUVars b2) => HasUVars (NestPair b1 b2) where freeUVars (NestPair b1 b2) = freeUVars b1 <> (freeUVars b2 `envDiff` boundUVars b1)