Make $ built in operation, rename ($) to apply
Slightly controversial, but I think it is better this way.
Main advantage:
Plays much better with disambiguation (which doesn't work especially
well with HOFs since it looks at the goal type and the types of each
argument to disambiguate, and if a function is the argument to $ we've
lost some of that information). This will make elaboration quicker in
some cases. $ is quite handy notation and we don't want to discourage it
just because it slows down the elaborator.
Main disadvantage:
Very occasional use in HOFs itself. Hence the new function 'apply' which
does the same thing.
commit865bf99906c1bfe1d979b334c9f377cde539eefa
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 18 Jan 2014, 19:45 (13 years ago)
parentec4ccc9
libs/prelude/Prelude.idr+2−2
@@ -275,11 +275,11 @@ instance Applicative List where
275275instance Applicative (Vect k) where
276276 pure = replicate _
277277
278− fs <$> vs = zipWith ($) fs vs
278+ fs <$> vs = zipWith apply fs vs
279279
280280instance Applicative Stream where
281281 pure = repeat
282− (<$>) = zipWith ($)
282+ (<$>) = zipWith apply
283283
284284---- Alternative instances
285285
libs/prelude/Prelude/Basics.idr+2−4
@@ -33,11 +33,9 @@ infixl 9 .
3333flip : (a -> b -> c) -> b -> a -> c
3434flip f x y = f y x
3535
36−infixr 1 $
37−
3836-- | Function application.
39−($) : (a -> b) -> a -> b
40−f $ a = f a
37+apply : (a -> b) -> a -> b
38+apply f a = f a
4139
4240cong : {f : t -> u} -> (a = b) -> f a = f b
4341cong refl = refl
src/Idris/ParseOps.hs+1
@@ -37,6 +37,7 @@ table fixes
3737 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
3838 ++ toTable (reverse fixes) ++
3939 [[backtick],
40+ [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],
4041 [binary "=" PEq AssocLeft],
4142 [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]
4243