diff --git a/autoapply.cabal b/autoapply.cabal --- a/autoapply.cabal +++ b/autoapply.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 0ebb847d015afb16b8a577b0a6012c39b43d5c5ac92fd9584450922c1f5d0730 +-- hash: 7dfbb655fdf55d5ab82b9457125299eaba2c2a4b318c4713df711e9c1ce23937 name: autoapply -version: 0.2.0.0 +version: 0.3 synopsis: Template Haskell to automatically pass values to functions description: See readme.md category: Template Haskell @@ -43,11 +43,11 @@ default-extensions: DeriveFoldable DeriveFunctor DeriveTraversable DerivingStrategies FlexibleContexts KindSignatures LambdaCase PatternSynonyms RankNTypes RecordWildCards ScopedTypeVariables TemplateHaskellQuotes TupleSections TypeApplications TypeFamilies ViewPatterns ghc-options: -Wall build-depends: - base >=4.13 && <5 + base >=4.9 && <5 , logict , mtl , template-haskell - , th-desugar >=1.10 + , th-desugar >=1.11 && <1.12 , transformers , unification-fd default-language: Haskell2010 diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -2,6 +2,9 @@ ## WIP +## [0.3] - 2020-05-06 + - Check constraints on functions + ## [0.2.0.0] - 2020-05-01 - Allow instantiating a polymorphic return type as a monadic value. For example `autoapply '[getFooIO] (bar :: Foo -> b)` will have type `IO b`. diff --git a/default.nix b/default.nix --- a/default.nix +++ b/default.nix @@ -13,7 +13,9 @@ haskellPackages = with pkgs.haskell.lib; pkgs.haskell.packages.${compiler'}.override { overrides = self: super: - { } // pkgs.lib.optionalAttrs hoogle { + { + th-desugar = self.callHackage "th-desugar" "1.11" { }; + } // pkgs.lib.optionalAttrs hoogle { ghc = super.ghc // { withPackages = super.ghc.withHoogle; }; ghcWithPackages = self.ghc.withPackages; }; diff --git a/readme.md b/readme.md --- a/readme.md +++ b/readme.md @@ -107,8 +107,8 @@ `template-haskell`'s `reifyInstances`. i.e. only the instance heads are checked. -Aside for checking for a `Monad` instance, no constraints are checked. So `autoapply` -will happily pass `reverse` to `(+)` yielding a value of type `Num ([a] -> [a]) => [a] -> [a]`. +Constraints are checked (up to `reifyInstances`) so it won't pass `reverse` to +`(+)` for example. Monadic binds are performed in the order of arguments passed to the wrapped function, and will be performed more than once if the argument is used multiple diff --git a/src/AutoApply.hs b/src/AutoApply.hs --- a/src/AutoApply.hs +++ b/src/AutoApply.hs @@ -1,3 +1,4 @@ +{-# language CPP #-} module AutoApply ( autoapply , autoapplyDecs @@ -6,6 +7,11 @@ import Control.Applicative import Control.Arrow ( (>>>) ) import Control.Monad +#if __GLASGOW_HASKELL__ < 808 +-- Control.Monad.Fail import is redundant since GHC 8.8.1 +import Control.Monad.Fail ( MonadFail + ) +#endif import Control.Monad.Logic ( LogicT , observeManyT ) @@ -21,6 +27,7 @@ import Data.Traversable import Language.Haskell.TH import Language.Haskell.TH.Desugar +import Prelude hiding ( pred ) -- | @autoapply args fun@ creates an expression which is equal to @fun@ applied -- to as many of the values in @args@ as possible. @@ -72,83 +79,124 @@ -- - If nothing matches we just use an 'Argument' -- - Take the first result of all these tries - let (fmap varBndrName -> cmdVarNames, _preds, args, ret) = - unravel (fType fun) - defaultMaybe m = (Just <$> m) <|> pure Nothing - liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a - liftQ = T.lift . T.lift - errorToLogic go = runExceptT go >>= \case - Left (_ :: UFailure TypeF IntVar) -> empty - Right x -> pure x + let + (fmap varBndrName -> cmdVarNames, preds, args, ret) = unravel (fType fun) + defaultMaybe m = (Just <$> m) <|> pure Nothing + liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a + liftQ = T.lift . T.lift + errorToLogic go = runExceptT go >>= \case + Left (_ :: UFailure TypeF IntVar) -> empty + Right x -> pure x + -- Quant will invent new variable names for any unification variables + -- still free + quant t = do + vs <- getFreeVars t + for_ vs $ \v -> bindVar v . (UTerm . VarF) =<< liftQ (newName "a") - -- Use LogicT so we can backtrack on failure - genProvs :: LogicT Q [ArgProvenance] - genProvs = evalIntBindingT $ do - cmdVars <- sequence [ (n, ) <$> freeVar | n <- cmdVarNames ] - instArgs <- traverse - (fmap (instWithVars cmdVars . snd) . liftQ . typeDtoF) - args - cmdM <- UVar <$> freeVar - retInst <- fmap (instWithVars cmdVars . snd) . liftQ . typeDtoF $ ret + -- Use LogicT so we can backtrack on failure + genProvs :: LogicT Q [ArgProvenance] + genProvs = evalIntBindingT $ do + cmdVars <- sequence [ (n, ) <$> freeVar | n <- cmdVarNames ] + instArgs <- traverse + (fmap (instWithVars cmdVars . snd) . liftQ . typeDtoF) + args - -- A list of - -- ( type to unify - -- , predicate to use this match - -- , the given providing the value - -- ) - -- - -- The predicate is there to make sure we only match unifiable monads - instGivens <- fmap concat . for givens $ \g@Given {..} -> do - -- The Given applied as is - nonApp <- do - instTy <- uncurry inst <=< liftQ . typeDtoF $ gType - v <- liftQ $ newName "g" - pure (instTy, pure (), BoundPure v g) - -- The given, but in an applicative context, only possible if we can - -- unify the monad and there is a Monad instance - app <- case stripForall gType of - (vars, DAppT m a) -> - liftQ (isInstance ''Applicative [sweeten m]) >>= \case - False -> pure Nothing - True -> do - m' <- inst vars . snd <=< liftQ . typeDtoF $ m - a' <- inst vars . snd <=< liftQ . typeDtoF $ a - v <- liftQ $ newName "g" - let predicate = do - _ <- unify m' cmdM - pure () - pure $ Just (a', predicate, Bound v g) - _ -> pure Nothing - pure ([nonApp] <> toList app) + cmdM <- UVar <$> freeVar + retInst <- fmap (instWithVars cmdVars . snd) . liftQ . typeDtoF $ ret - as <- for instArgs $ \argTy -> - defaultMaybe . asum $ instGivens <&> \(givenTy, predicate, g) -> do - _ <- errorToLogic $ do - predicate - freshGivenTy <- freshen givenTy - unify freshGivenTy argTy - pure g + -- A list of + -- ( type to unify + -- , predicate to use this match + -- , the given providing the value + -- ) + -- + -- The predicate is there to make sure we only match unifiable monads + instGivens <- fmap concat . for givens $ \g@Given {..} -> do + -- The Given applied as is + nonApp <- do + instTy <- uncurry inst <=< liftQ . typeDtoF $ gType + v <- liftQ $ newName "g" + pure (instTy, pure (), BoundPure v g) + -- The given, but in an applicative context, only possible if we can + -- unify the monad and there is a Monad instance + app <- case stripForall gType of + (vars, DAppT m a) -> + liftQ (isInstance ''Applicative [sweeten m]) >>= \case + False -> pure Nothing + True -> do + m' <- inst vars . snd <=< liftQ . typeDtoF $ m + a' <- inst vars . snd <=< liftQ . typeDtoF $ a + v <- liftQ $ newName "g" + let predicate = do + _ <- unify m' cmdM + pure () + pure $ Just (a', predicate, Bound v g) + _ -> pure Nothing + pure ([nonApp] <> toList app) - -- If we used any monadic bindings, we must have a Monad instance for - -- the return variable. If it's polymorphic then assume an instance. - when (any isMonadicBind (catMaybes as)) $ do - a <- UVar <$> freeVar - ret' <- errorToLogic $ unify retInst (UTerm (AppF cmdM a)) - retFrozen <- freeze <$> errorToLogic (applyBindings ret') - case retFrozen of - Just (Fix (AppF m _)) -> do - let typeD = typeFtoD m - liftQ (isInstance ''Applicative [sweeten typeD]) >>= \case - False -> empty - True -> pure () - Nothing -> pure () - _ -> empty + as <- for instArgs $ \argTy -> + defaultMaybe . asum $ instGivens <&> \(givenTy, predicate, g) -> do + _ <- errorToLogic $ do + predicate + freshGivenTy <- freshen givenTy + unify freshGivenTy argTy + pure g - for (zip args as) $ \case - (_, Just p ) -> pure p - (t, Nothing) -> (`Argument` t) <$> liftQ (newName "a") + -- If we used any monadic bindings, we must have a Monad instance for + -- the return variable. If it's polymorphic then assume an instance. + when (any isMonadicBind (catMaybes as)) $ do + a <- UVar <$> freeVar + ret' <- errorToLogic $ unify retInst (UTerm (AppF cmdM a)) + quant ret' + retFrozen <- freeze <$> errorToLogic (applyBindings ret') + case retFrozen of + Just (Fix (AppF m _)) -> do + let typeD = typeFtoD m + liftQ (isInstance ''Applicative [sweeten typeD]) >>= \case + False -> empty + True -> pure () + Nothing -> + liftQ + $ fail + "\"impossible\", return type didn't freeze while checking monadic bindings" + _ -> empty + -- Guard on all the instances being satisfiable + -- + -- This must come after the Monadic binding checker so that the (possibly + -- new) return type has been constrained a little. + for_ preds $ \pred -> do + + -- Get the constraint with the correct unification variables + instPred <- fmap (instWithVars cmdVars . snd) . liftQ . typeDtoF $ pred + + -- Quantify over any still free + quant instPred + + -- Freeze it + instFrozen <- freeze <$> errorToLogic (applyBindings instPred) + + case instFrozen of + Just f -> do + let (class', predArgs) = unfoldDType (typeFtoD f) + typeArgs = [ a | DTANormal a <- predArgs ] + className <- case class' of + DConT n -> pure n + _ -> liftQ $ fail "unfolded predicate didn't begin with a ConT" + liftQ (isInstance className (sweeten <$> typeArgs)) >>= \case + False -> empty + True -> pure () + Nothing -> + liftQ + $ fail + "\"impossible\": predicate didn't freeze while checking predicates" + + + for (zip args as) $ \case + (_, Just p ) -> pure p + (t, Nothing) -> (`Argument` t) <$> liftQ (newName "a") + argProvenances <- note "\"Impossible\" Finding argument provenances failed" . listToMaybe @@ -222,8 +270,9 @@ typeDtoF = traverse go . stripForall where go = \case - DForallT{} -> fail "TODO: Higher ranked types" - DAppT l r -> do + DForallT{} -> fail "TODO: Higher ranked types" + DConstrainedT{} -> fail "TODO: Higher ranked types" + DAppT l r -> do l' <- go l r' <- go r pure $ Fix (AppF l' r') @@ -252,11 +301,13 @@ -- -- For example @forall a. a -> forall b. b@ becomes @forall a b. a -> b@ raiseForalls :: DType -> DType -raiseForalls = uncurry3 DForallT . go +raiseForalls = go >>> \case + (vs, ctx, t) -> DForallT ForallVis vs . DConstrainedT ctx $ t where go = \case - DForallT vs ctx t -> - let (vs', ctx', t') = go t in (vs <> vs', ctx <> ctx', t') + DForallT _ vs t -> let (vs', ctx', t') = go t in (vs <> vs', ctx', t') + DConstrainedT ctx t -> + let (vs', ctx', t') = go t in (vs', ctx <> ctx', t') l :~> r -> let (vs, ctx, r') = go r in (vs, ctx, l :~> r') t -> ([], [], t) @@ -296,11 +347,20 @@ stripForall :: DType -> ([Name], DType) stripForall = raiseForalls >>> \case - DForallT vs _ ty -> (varBndrName <$> vs, ty) - ty -> ([], ty) + DForallT _ vs (DConstrainedT _ ty) -> (varBndrName <$> vs, ty) + DForallT _ vs ty -> (varBndrName <$> vs, ty) + DConstrainedT _ ty -> ([], ty) + ty -> ([], ty) -uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d -uncurry3 f (a, b, c) = f a b c +unravel :: DType -> ([DTyVarBndr], [DPred], [DType], DType) +unravel t = + let (argList, ret) = unravelDType t + go = \case + DFANil -> ([], [], []) + DFAForalls _ vs as -> (vs, [], []) <> go as + DFACxt preds as -> ([], preds, []) <> go as + DFAAnon a as -> ([], [], [a]) <> go as + in let (vs, preds, args) = go argList in (vs, preds, args, ret) note :: MonadFail m => String -> Maybe a -> m a note s = maybe (fail s) pure