idris 1.3.3 → 1.3.4
raw patch · 33 files changed
+75/−94 lines, 33 filesdep ~aesondep ~ansi-terminaldep ~base64-bytestring
Dependency ranges changed: aeson, ansi-terminal, base64-bytestring, haskeline, megaparsec, optparse-applicative
Files
- CHANGELOG.md +4/−0
- README.md +13/−6
- codegen/idris-codegen-node/Main.hs +0/−2
- idris.cabal +10/−10
- libs/base/Data/List/Views.idr +1/−1
- libs/contrib/Network/Socket.idr +3/−3
- rts/arduino/idris_main.c +3/−1
- src/IRTS/Compiler.hs +0/−1
- src/IRTS/JavaScript/Codegen.hs +0/−2
- src/IRTS/LangOpts.hs +0/−3
- src/IRTS/System.hs +0/−1
- src/Idris/CmdOptions.hs +0/−1
- src/Idris/Core/Binary.hs +0/−1
- src/Idris/Core/Elaborate.hs +3/−3
- src/Idris/Core/ProofState.hs +4/−5
- src/Idris/Core/TT.hs +4/−4
- src/Idris/Delaborate.hs +9/−5
- src/Idris/Docstrings.hs +0/−2
- src/Idris/Elab/Data.hs +0/−5
- src/Idris/Elab/Term.hs +2/−3
- src/Idris/Erasure.hs +4/−7
- src/Idris/IBC.hs +1/−1
- src/Idris/IdrisDoc.hs +0/−1
- src/Idris/Imports.hs +0/−1
- src/Idris/Output.hs +1/−9
- src/Idris/Package.hs +0/−1
- src/Idris/Parser/Data.hs +0/−1
- src/Idris/Parser/Stack.hs +4/−0
- src/Idris/ProofSearch.hs +0/−1
- src/Idris/REPL.hs +8/−8
- src/Idris/TypeSearch.hs +1/−3
- src/Util/DynamicLinker.hs +0/−1
- test/TestRun.hs +0/−1
CHANGELOG.md view
@@ -1,5 +1,9 @@ # New since last release +# New in 1.3.4++ Renamed 'forall' function for compability with future GHC releases++ Updated version bounds++ Bugfixes # New in 1.3.3 + Updated to work with GHC 8.8 and cabal 3.0 + Bugfixes and documentation updates
README.md view
@@ -1,4 +1,4 @@-# Idris+# Idris 1 [](https://travis-ci.org/idris-lang/Idris-dev) [](https://ci.appveyor.com/project/idrislang/idris-dev)@@ -11,7 +11,7 @@ Idris (https://idris-lang.org/) is a general-purpose functional programming language with dependent types. -## Installation Guides.+## Installation This repository represents the latest development version of the language, and may contain bugs that are being actively worked on. For@@ -26,10 +26,19 @@ Idris has support for external code generators. Supplied with the distribution is a C code generator to compile executables, and a JavaScript code generator-with support for node.js and browser JavaScript.+with support for `node.js` and browser JavaScript. -More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html).+More information about code generators can be found+[here](https://idris.readthedocs.io/en/latest/reference/codegen.html). +## Status++This is Idris 1, implemented in Haskell. Idris 1 is not actively+worked on anymore.++[Idris 2](https://github.com/idris-lang/Idris2) is the next generation+of Idris, and where primary development happens.+ ## More Information If you would like to find out more information, or ask questions, we@@ -45,5 +54,3 @@ For those interested in contributing to Idris directly we kindly ask that prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first. -[Idris 2](https://github.com/edwinb/Idris2) is an early preview of the next generation-of Idris, implemented in Idris.
codegen/idris-codegen-node/Main.hs view
@@ -7,8 +7,6 @@ import IRTS.CodegenJavaScript import IRTS.Compiler -import Paths_idris- import Control.Monad import System.Environment
idris.cabal view
@@ -1,6 +1,6 @@ Cabal-Version: 2.4 Name: idris-Version: 1.3.3+Version: 1.3.4 License: BSD-3-Clause License-file: LICENSE Author: Edwin Brady@@ -146,7 +146,7 @@ custom-setup setup-depends:- Cabal >= 2.4 && < 3.1,+ Cabal >= 2.4 && <= 3.4, base >= 4 && <5, directory, filepath,@@ -166,7 +166,7 @@ -- Defaults to True because Hackage is a source release Flag release Description: This is an official release- Default: True+ Default: False manual: True Flag freestanding@@ -319,12 +319,12 @@ , BuildFlags_idris Build-depends: base >=4 && <5- , aeson >= 0.6 && < 1.5+ , aeson >= 0.6 && < 1.6 , annotated-wl-pprint >= 0.7 && < 0.8- , ansi-terminal < 0.11+ , ansi-terminal < 0.12 , ansi-wl-pprint < 0.7 , array >= 0.4.0.1 && < 0.6- , base64-bytestring < 1.2+ , base64-bytestring < 1.3 , binary >= 0.8.4.1 && < 0.9 , blaze-html >= 0.6.1.3 && < 0.10 , blaze-markup >= 0.5.2.1 && < 0.10@@ -336,12 +336,12 @@ , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0 , filepath < 1.5 , fingertree >= 0.1.4.1 && < 0.2- , haskeline >= 0.7 && < 0.8+ , haskeline >= 0.8 && < 0.9 , ieee754 >= 0.7 && < 0.9- , megaparsec >= 7.0.4 && < 9+ , megaparsec >= 7.0.4 && < 10 , mtl >= 2.1 && < 2.3 , network >= 2.7 && < 3.1.2- , optparse-applicative >= 0.13 && < 0.16+ , optparse-applicative >= 0.13 && < 0.17 , parser-combinators >= 1.0.0 , pretty < 1.2 , process < 1.7@@ -416,7 +416,7 @@ , filepath , directory , haskeline >= 0.7- , optparse-applicative >= 0.13 && < 0.16+ , optparse-applicative >= 0.13 && < 0.17 , tagged , tasty >= 0.8 , tasty-golden >= 2.0
libs/base/Data/List/Views.idr view
@@ -28,7 +28,7 @@ data Split : List a -> Type where SplitNil : Split [] SplitOne : Split [x]- SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae+ SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erase Split (x :: xs ++ y :: ys) splitHelp : (head : a) ->
libs/contrib/Network/Socket.idr view
@@ -178,10 +178,10 @@ recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of- Left 0 => pure (Right $ concat $ reverse acc) Left c => pure (Left c)- Right (str, _) => let n' = min (n * 2) 65536 in- recvRec sock (str :: acc) n'+ Right (str, res) => let n' = min (n * 2) 65536 in+ if res < n then pure (Right $ concat $ reverse $ str :: acc)+ else recvRec sock (str :: acc) n' ||| Send a message. |||
rts/arduino/idris_main.c view
@@ -3,6 +3,8 @@ #include "idris_rts.h" #include "Arduino.h" +void* _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);+ // The default options should give satisfactory results under many circumstances. RTSOpts opts = { .init_heap_size = 128,@@ -15,7 +17,7 @@ init(); // arduino init function VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1);- _idris__123_runMain0_125_(vm, NULL);+ _idris__123_runMain_95_0_125_(vm, NULL); #ifdef IDRIS_DEBUG if (opts.show_summary) {
src/IRTS/Compiler.hs view
@@ -35,7 +35,6 @@ import Control.Monad.State import Data.List import qualified Data.Map as M-import Data.Maybe (maybe) import Data.Ord import qualified Data.Set as S import System.Directory
src/IRTS/JavaScript/Codegen.hs view
@@ -23,10 +23,8 @@ import IRTS.Lang import IRTS.System -import Control.Applicative (pure, (<$>)) import Control.Monad import Control.Monad.Trans.State-import Data.Foldable (foldMap) import Data.Generics.Uniplate.Data import Data.List import Data.Map.Strict (Map)
src/IRTS/LangOpts.hs view
@@ -14,9 +14,6 @@ import IRTS.Lang import Control.Monad.State hiding (lift)-import Data.List--import Debug.Trace inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)] inlineAll lds = let defs = addAlist lds emptyContext in
src/IRTS/System.hs view
@@ -27,7 +27,6 @@ #endif import BuildFlags_idris -import Control.Applicative ((<$>)) import Data.List.Split import Data.Maybe (fromMaybe) import System.Environment
src/Idris/CmdOptions.hs view
@@ -24,7 +24,6 @@ import Control.Monad.Trans.Reader (ask) import Data.Char import Data.Maybe-import Data.Monoid ((<>)) import Options.Applicative import Options.Applicative.Arrows import Options.Applicative.Types (ReadM(..))
src/Idris/Core/Binary.hs view
@@ -12,7 +12,6 @@ import Idris.Core.TT -import Control.Applicative ((<$>), (<*>)) import Data.Binary import Data.Binary.Get import Data.Binary.Put
src/Idris/Core/Elaborate.hs view
@@ -434,8 +434,8 @@ introTy :: Raw -> Maybe Name -> Elab' aux () introTy ty n = processTactic' (IntroTy ty n) -forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()-forall n r i t = processTactic' (Forall n r i t)+forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()+forAll n r i t = processTactic' (Forall n r i t) letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux () letbind n rig t v = processTactic' (LetBind n rig t v)@@ -823,7 +823,7 @@ arg n r i tyhole = do ty <- unique_hole tyhole claim ty RType movelast ty- forall n r i (Var ty)+ forAll n r i (Var ty) -- try a tactic, if it adds any unification problem, return an error no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()
src/Idris/Core/ProofState.hs view
@@ -28,7 +28,6 @@ import Util.Pretty hiding (fill) -import Control.Arrow ((***)) import Control.Monad.State.Strict import Data.List @@ -659,13 +658,13 @@ _ -> lift $ tfail $ CantIntroduce t' intro n ctxt env _ = fail "Can't introduce here." -forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic-forall n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =+forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic+forAll n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do (tyv, tyt) <- lift $ check ctxt env ty unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing) unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing) return $ Bind n (Pi rig impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))-forall n rig impl ty ctxt env _ = fail "Can't pi bind here"+forAll n rig impl ty ctxt env _ = fail "Can't pi bind here" patvar :: Name -> RunTactic patvar n ctxt env (Bind x (Hole t) sc) =@@ -1053,7 +1052,7 @@ mktac WHNF_ComputeArgs = whnf_compute_args mktac (Intro n) = intro n mktac (IntroTy ty n) = introTy ty n- mktac (Forall n r i t) = forall n r i t+ mktac (Forall n r i t) = forAll n r i t mktac (LetBind n r t v) = letbind n r t v mktac (ExpandLet n b) = expandLet n b mktac (Rewrite t) = rewrite t
src/Idris/Core/TT.hs view
@@ -58,10 +58,10 @@ import Util.Pretty hiding (Str) -- Work around AMP without CPP-import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,- Integer, Maybe(..), Monad(..), Monoid(..), Num(..), Ord(..),- Ordering(..), Show(..), String, div, error, fst, max, min, mod,- not, otherwise, read, snd, ($), (&&), (.), (||))+import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Int, Integer,+ Maybe(..), Monoid(..), Num(..), Ord(..), Ordering(..), Show(..),+ String, div, error, fst, max, min, mod, not, otherwise, read,+ snd, ($), (&&), (.), (||)) #if (MIN_VERSION_base(4,11,0)) import qualified Prelude as S (Semigroup(..))
src/Idris/Delaborate.hs view
@@ -10,7 +10,7 @@ module Idris.Delaborate ( annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab- , pprintDelabTy, pprintErr, resugar+ , pprintDelabTy', pprintDelabTy, pprintErr, resugar ) where import Idris.AbsSyntax@@ -283,14 +283,18 @@ pprintNoDelab ist tm = annotate (AnnTerm [] tm) (prettyIst ist (delab ist tm)) +pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation+pprintDelabTy' i n ty+ = annotate (AnnTerm [] ty) . prettyIst i $+ case lookupCtxt n (idris_implicits i) of+ (imps:_) -> resugar i $ delabTy' i imps [] ty False False True+ _ -> resugar i $ delabTy' i [] [] ty False False True+ -- | Pretty-print the type of some name pprintDelabTy :: IState -> Name -> Doc OutputAnnotation pprintDelabTy i n = case lookupTy n (tt_ctxt i) of- (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $- case lookupCtxt n (idris_implicits i) of- (imps:_) -> resugar i $ delabTy' i imps [] ty False False True- _ -> resugar i $ delabTy' i [] [] ty False False True+ (ty:_) -> pprintDelabTy' i n ty [] -> error "pprintDelabTy got a name that doesn't exist" pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
src/Idris/Docstrings.hs view
@@ -27,11 +27,9 @@ import qualified Cheapskate as C import Cheapskate.Html (renderDoc) import qualified Cheapskate.Types as CT-import Data.Foldable (Foldable) import qualified Data.Foldable as F import qualified Data.Sequence as S import qualified Data.Text as T-import Data.Traversable (Traversable) import GHC.Generics (Generic) import Text.Blaze.Html (Html)
src/Idris/Elab/Data.hs view
@@ -32,13 +32,8 @@ import Control.Category import Control.Monad-import Control.Monad.State.Strict as State-import Data.Char (isLetter, toLower) import Data.List-import qualified Data.Map as Map-import Data.Maybe import qualified Data.Set as S-import qualified Data.Text as T warnLC :: FC -> Name -> Idris () warnLC fc n
src/Idris/Elab/Term.hs view
@@ -30,7 +30,6 @@ import Idris.Reflection import Idris.Termination (buildSCG, checkDeclTotality, checkPositive) -import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.Foldable (for_)@@ -686,7 +685,7 @@ _ -> unless (LinearTypes `elem` idris_language_extensions ist || e_qq ina) $ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")- forall n' (pcount p) (is_scoped p) (Var tyn)+ forAll n' (pcount p) (is_scoped p) (Var tyn) addAutoBind p n' addPSname n' -- okay for proof search focus tyn@@ -2108,7 +2107,7 @@ = do ~[n, ty] <- tacTmArgs 2 tac args n' <- reifyTTName n ty' <- reifyRaw ty- forall n' RigW Nothing ty'+ forAll n' RigW Nothing ty' returnUnit | n == tacN "Prim__PatVar" = do ~[n] <- tacTmArgs 1 tac args
src/Idris/Erasure.hs view
@@ -607,16 +607,13 @@ -- convert applications of lambdas to lets -- note that this transformation preserves de bruijn numbering lamToLet :: Term -> Term- lamToLet tm = lamToLet' args f+ lamToLet tm = lamToLet' 0 args f where (f, args) = unApply tm - lamToLet' :: [Term] -> Term -> Term- lamToLet' (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty v) $ lamToLet' vs tm- lamToLet' [] tm = tm- lamToLet' vs tm = error $- "Erasure.hs:lamToLet': unexpected input: "- ++ "vs = " ++ show vs ++ ", tm = " ++ show tm+ lamToLet' :: Int -> [Term] -> Term -> Term+ lamToLet' wk (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty (weakenTm wk v)) $ lamToLet' (wk+1) vs tm+ lamToLet' wk vs tm = mkApp tm $ map (weakenTm wk) vs -- split "\x_i -> T(x_i)" into [x_i] and T unfoldLams :: Term -> ([Name], Term)
src/Idris/IBC.hs view
@@ -41,7 +41,7 @@ import System.FilePath ibcVersion :: Word16-ibcVersion = 166+ibcVersion = 167 -- | When IBC is being loaded - we'll load different things (and omit -- different structures/definitions) depending on which phase we're in.
src/Idris/IdrisDoc.hs view
@@ -29,7 +29,6 @@ import qualified Data.List as L import qualified Data.Map as M hiding ((!)) import Data.Maybe-import Data.Monoid (mempty) import qualified Data.Set as S import qualified Data.Text as T import System.Directory
src/Idris/Imports.hs view
@@ -16,7 +16,6 @@ import Idris.Error import IRTS.System (getIdrisLibDir) -import Control.Applicative ((<$>)) import Control.Monad.State.Strict import Data.Char (isAlpha, isDigit, toLower) import Data.List (isSuffixOf)
src/Idris/Output.hs view
@@ -37,21 +37,13 @@ #endif import Control.Arrow (first)-import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT) import Data.List (intersperse, nub) import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe) import qualified Data.Set as S-import System.Console.Haskeline.MonadException (MonadException(controlIO),- RunIO(RunIO)) import System.FilePath (replaceExtension) import System.IO (Handle, hPutStr, hPutStrLn) import System.IO.Error (tryIOError) -instance MonadException m => MonadException (ExceptT Err m) where- controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let- run' = RunIO (fmap ExceptT . run . runExceptT)- in fmap runExceptT $ f run'- pshow :: IState -> Err -> String pshow ist err = displayDecorated (consoleDecorate ist) . renderPretty 1.0 80 .@@ -319,7 +311,7 @@ iputStr s = do i <- getIState case idris_outputmode i of RawOutput h -> runIO $ hPutStr h s- IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n idemodePutSExp :: SExpable a => String -> a -> Idris () idemodePutSExp cmd info = do i <- getIState
src/Idris/Package.hs view
@@ -9,7 +9,6 @@ module Idris.Package where import System.Directory-import System.Directory (copyFile, createDirectoryIfMissing) import System.Environment import System.Exit import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
src/Idris/Parser/Data.hs view
@@ -12,7 +12,6 @@ import Idris.AbsSyntax import Idris.Core.TT import Idris.Docstrings-import Idris.Options import Idris.Parser.Expr import Idris.Parser.Helpers import Idris.Parser.Ops
src/Idris/Parser/Stack.hs view
@@ -84,7 +84,11 @@ (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err) #endif messageText = PP.text . init . P.parseErrorTextPretty . parseError+#if MIN_VERSION_megaparsec(9,0,0)+ messageSource err = sline+#else messageSource err = Just sline+#endif where #if MIN_VERSION_megaparsec(8,0,0) (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
src/Idris/ProofSearch.hs view
@@ -22,7 +22,6 @@ import Idris.Core.Unify import Idris.Delaborate -import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.List
src/Idris/REPL.hs view
@@ -122,23 +122,21 @@ (if colour && not isWindows then colourisePrompt theme str else str) ++ " "- x <- H.catch (H.withInterrupt $ getInputLine prompt)- (ctrlC (return $ Just ""))+ x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt) case x of Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye") return () Just input -> -- H.catch- do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)- (ctrlC (return (Just mods)))+ do ms <- H.handleInterrupt (ctrlC (return (Just mods))) (H.withInterrupt $ lift $ processInput input orig mods efile) case ms of Just mods -> let efile' = fromMaybe efile (listToMaybe mods) in repl orig mods efile' Nothing -> return () -- ctrlC) -- ctrlC- where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a- ctrlC act e = do lift $ iputStrLn (show e)- act -- repl orig mods+ where ctrlC :: InputT Idris a -> InputT Idris a+ ctrlC act = do lift $ iputStrLn "Interrupted"+ act -- repl orig mods showMVs c thm [] = "" showMVs c thm ms = "Holes: " ++@@ -258,6 +256,7 @@ idemodeStart s orig mods = do h <- runIO $ if s then initIdemodeSocket else return stdout setIdeMode True h+ runIO $ hSetNewlineMode h (NewlineMode { inputNL = CRLF, outputNL = LF }) i <- getIState case idris_outputmode i of IdeMode n h ->@@ -517,7 +516,7 @@ prettyName True False [] n <> case lookupTyExact n ctxt of Just t ->- space <> colon <> space <> align (group (pprintDelab ist t))+ space <> colon <> space <> align (group (pprintDelabTy' ist n t)) Nothing -> empty @@ -682,6 +681,7 @@ iPrintResult "" idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a) iPrintResult ""+idemodeProcess fn (Browse ns) = process fn (Browse ns) idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n) idemodeProcess fn (CallsWho n) = process fn (CallsWho n) idemodeProcess fn (PrintDef n) = process fn (PrintDef n)
src/Idris/TypeSearch.hs view
@@ -38,20 +38,18 @@ #else import Prelude hiding (pred) #endif-import Control.Applicative (Applicative(..), (<$>), (<*>), (<|>))+import Control.Applicative ((<|>)) import Control.Arrow (first, second, (&&&), (***)) import Control.Monad (guard, when) import Data.List (find, partition, (\\)) import Data.Map (Map) import qualified Data.Map as M import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe, maybeToList)-import Data.Monoid (Monoid(mappend, mempty)) import Data.Ord (comparing) import qualified Data.PriorityQueue.FingerTree as Q import Data.Set (Set) import qualified Data.Set as S import qualified Data.Text as T (isPrefixOf, pack)-import Data.Traversable (traverse) searchByType :: [PkgName] -> PTerm -> Idris () searchByType pkgs pterm = do
src/Util/DynamicLinker.hs view
@@ -25,7 +25,6 @@ import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr) #ifdef linux_HOST_OS import Data.Array (bounds, inRange, (!))-import Data.Functor ((<$>)) import Data.Maybe (catMaybes) #else import Data.Array (bounds, (!))
test/TestRun.hs view
@@ -6,7 +6,6 @@ import Control.Monad import Data.Char (isLetter) import qualified Data.IntMap as IMap-import Data.Monoid ((<>)) import Data.Proxy import Data.Typeable import Options.Applicative