6df52fa · Idris-dev · git.iko.soy

docs/faq/faq.rst+11−7

compare with master

unifiedsplit

@@ -5,13 +5,17 @@ Frequently Asked Questions

5What are the differences between Agda and Idris?

6================================================

7

8+Like Idris, Agda is a functional language with dependent types, supporting

9+dependent pattern matching. Both can be used for writing programs and proofs.

8−The main difference is that Idris has been designed from the start to support

10+However, Idris has been designed from the start to emphasise general purpose

9−verified systems programming through easy interoperability with C and high

10−level language constructs to support domain specific language implementation.

11−Idris emphasises general-purpose programming, rather than theorem proving, and

11+programming rather than theorem proving. As such, it supports interoperability

12+with systems libraries and C programs, and language constructs for

13+domain specific language implementation. It also includes higher level

12−as such includes higher level programming constructs such as type classes and

14+programming constructs such as type classes and do notation.

13−do notation. Idris also supports tactic based theorem proving, and has a

15+

14−lightweight Hugs/GHCI style interface.

16+Idris supports multiple back ends (C and JavaScript by default, with the

17+ability to add more via plugins) and has a reference run time system, written

18+in C, with a garbage collector and built-in message passing concurrency.

15

19

16Is Idris production ready?

20Is Idris production ready?

17==========================

21==========================

docs/tutorial/typesfuns.rst+5−5

@@ -268,8 +268,8 @@ can be used to calculate a return type:

268.. code-block:: idris

269

270 mkSingle : (x : Bool) -> isSingleton x

271− mkSingle False = 0

271+ mkSingle True = 0

272− mkSingle True = []

272+ mkSingle False = []

273

274Or it can be used to have varying input types. The following function

275calculates either the sum of a list of ``Nat``, or returns the given

@@ -278,9 +278,9 @@ calculates either the sum of a list of ``Nat``, or returns the given

278.. code-block:: idris

279

280 sum : (single : Bool) -> isSingleton single -> Nat

281− sum False x = x

281+ sum True x = x

282− sum True [] = 0

282+ sum False [] = 0

283− sum True (x :: xs) = x + sum True xs

283+ sum False (x :: xs) = x + sum False xs

284

285Vectors

286-------

libs/base/Control/Monad/State.idr+1−1

@@ -1,7 +1,7 @@

1module Control.Monad.State

2

3import public Control.Monad.Identity

4−import Control.Monad.Trans

4+import public Control.Monad.Trans

5

6%access public

7

libs/effects/Effect/Monad.idr+19−12

@@ -2,20 +2,27 @@ module Effect.Monad

2

3import Effects

4

5−-- Eff is a monad too, so we can happily use it in a monad transformer.

5+data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where

6+ MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

6

7

7−using (xs : List EFFECT, m : Type -> Type)

8− instance Functor (\a => EffM m a xs (\v => xs)) where

8+instance Functor (MonadEffT xs f) where

9− map f prog = do t <- prog

9+ map f (MkMonadEffT x) = MkMonadEffT (do x' <- x

10− value (f t)

10+ pure (f x'))

11

12− instance Applicative (\a => EffM m a xs (\v => xs)) where

12+instance Applicative (MonadEffT xs f) where

13− pure = value

13+ pure x = MkMonadEffT (pure x)

14− (<*>) f a = do f' <- f

14+ (<*>) (MkMonadEffT f) (MkMonadEffT x)

15− a' <- a

15+ = MkMonadEffT (do f' <- f

16− value (f' a')

16+ x' <- x

17+ pure (f' x'))

17

18

18− instance Monad (\a => Eff m a xs (\v => xs)) where

19+instance Monad (MonadEffT xs f) where

19− (>>=) = Effects.(>>=)

20+ (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x

21+ let MkMonadEffT fx = f x'

22+ fx)

20

23

24+implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

25+monadEffT = MkMonadEffT

21

26

27+MonadEff : List EFFECT -> Type -> Type

28+MonadEff xs = MonadEffT xs id

libs/effects/Effect/Trans.idrnew file+20

@@ -0,0 +1,20 @@

1+module Effect.Trans

2+

3+import Effects

4+

5+%access public

6+

7+data Trans : (Type -> Type) -> Effect where

8+ Lift : m a -> sig (Trans m) a

9+

10+-- using (m : Type -> Type)

11+instance Monad m => Handler (Trans m) m where

12+ handle st (Lift op) k = do x <- op

13+ k x ()

14+

15+TRANS : (Type -> Type) -> EFFECT

16+TRANS m = MkEff () (Trans m)

17+

18+lift : m a -> Eff a [TRANS m]

19+lift op = call $ Lift op

20+

libs/effects/effects.ipkg+2−2

@@ -1,9 +1,9 @@

1package effects

2

3opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = Effects, Effect.Default,

4+modules = Effects, Effect.Default, Effect.Monad,

5

6 Effect.Exception, Effect.File, Effect.State,

7 Effect.Random, Effect.StdIO, Effect.Select,

8− Effect.Memory, Effect.System

8+ Effect.Memory, Effect.System, Effect.Trans

9

src/Idris/Docs.hs+25−10

@@ -53,17 +53,26 @@ showDoc ist d

53 | otherwise = text " -- " <>

54 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d

55

56−pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

56+pprintFD :: IState -> Bool -> FunDoc -> Doc OutputAnnotation

57−pprintFD ist (FD n doc args ty f)

57+pprintFD ist totalityFlag (FD n doc args ty f)

58 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

59 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

60 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

61+ -- show doc

61 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>

62 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>

63+ -- show fixity

62 maybe empty (\f -> text (show f) <> line) f <>

64 maybe empty (\f -> text (show f) <> line) f <>

65+ -- show arguments doc

63 let argshow = showArgs args [] in

66 let argshow = showArgs args [] in

64− if not (null argshow)

67+ (if not (null argshow)

65 then nest 4 $ text "Arguments:" <$> vsep argshow

68 then nest 4 $ text "Arguments:" <$> vsep argshow

66− else empty)

69+ else empty) <>

70+ -- show totality status

71+ let totality = getTotality in

72+ (if totalityFlag && not (null totality) then

73+ line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)

74+ else

75+ empty))

67

76

68 where ppo = ppOptionIst ist

77 where ppo = ppOptionIst ist

69 infixes = idris_infixes ist

78 infixes = idris_infixes ist

@@ -87,15 +96,21 @@ pprintFD ist (FD n doc args ty f)

87 showArgs args ((n, True):bnd)

96 showArgs args ((n, True):bnd)

88 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

97 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

89 showArgs [] _ = []

98 showArgs [] _ = []

99+ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)

90

100

101+pprintFDWithTotality :: IState -> FunDoc -> Doc OutputAnnotation

102+pprintFDWithTotality ist = pprintFD ist True

103+

104+pprintFDWithoutTotality :: IState -> FunDoc -> Doc OutputAnnotation

105+pprintFDWithoutTotality ist = pprintFD ist False

91

106

92pprintDocs :: IState -> Docs -> Doc OutputAnnotation

107pprintDocs :: IState -> Docs -> Doc OutputAnnotation

93−pprintDocs ist (FunDoc d) = pprintFD ist d

108+pprintDocs ist (FunDoc d) = pprintFDWithTotality ist d

94pprintDocs ist (DataDoc t args)

109pprintDocs ist (DataDoc t args)

95− = text "Data type" <+> pprintFD ist t <$>

110+ = text "Data type" <+> pprintFDWithoutTotality ist t <$>

96 if null args then text "No constructors."

111 if null args then text "No constructors."

97 else nest 4 (text "Constructors:" <> line <>

112 else nest 4 (text "Constructors:" <> line <>

98− vsep (map (pprintFD ist) args))

113+ vsep (map (pprintFDWithoutTotality ist) args))

99pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)

114pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)

100 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

115 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

101 if nullDocstring doc

116 if nullDocstring doc

@@ -105,12 +120,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

105 nest 4 (text "Parameters:" <$> prettyParameters)

120 nest 4 (text "Parameters:" <$> prettyParameters)

106 <> line <$>

121 <> line <$>

107 nest 4 (text "Methods:" <$>

122 nest 4 (text "Methods:" <$>

108− vsep (map (pprintFD ist) meths))

123+ vsep (map (pprintFDWithTotality ist) meths))

109 <$>

124 <$>

110 maybe empty

125 maybe empty

111 ((<> line) . nest 4 .

126 ((<> line) . nest 4 .

112 (text "Instance constructor:" <$>) .

127 (text "Instance constructor:" <$>) .

113− pprintFD ist)

128+ pprintFDWithoutTotality ist)

114 ctor

129 ctor

115 <>

130 <>

116 nest 4 (text "Instances:" <$>

131 nest 4 (text "Instances:" <$>

@@ -195,7 +210,7 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

195 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

210 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

196

211

197pprintDocs ist (NamedInstanceDoc _cls doc)

212pprintDocs ist (NamedInstanceDoc _cls doc)

198− = nest 4 (text "Named instance:" <$> pprintFD ist doc)

213+ = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist doc)

199

214

200pprintDocs ist (ModDoc mod docs)

215pprintDocs ist (ModDoc mod docs)

201 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

216 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

test/classes001/expected+2

@@ -8,6 +8,7 @@ Methods:

8 myShow : MyShow a => (x : a) -> String

9 The shower

10

11+ The function is Total

11Instance constructor:

12Instance constructor:

12 MkMyShow : (myShow : a -> String) -> MyShow a

13 MkMyShow : (myShow : a -> String) -> MyShow a

13 Build a MyShow

14 Build a MyShow

@@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a

25

26

26 myShow : a -> String -- The shower

27 myShow : a -> String -- The shower

27

28

29+ The function is Total

test/docs001/expected+1

@@ -8,6 +8,7 @@ Methods:

8 m : C t => t

9 member of class

10

11+ The function is Total

11Instances:

12Instances:

12 C A

13 C A

13 instance of class

14 instance of class

test/docs002/expected+3

@@ -1,9 +1,12 @@

1T1 : Type

2 Some documentation

3

4+ The function is Total

4T2 : Type

5T2 : Type

5 Some other documentation

6 Some other documentation

6

7

8+ The function is Total

7T3 : Int

9T3 : Int

8 Some provided postulate

10 Some provided postulate

9

11

12+ The function is not yet checked for totality

test/docs003/expected+1

@@ -8,6 +8,7 @@ Methods:

8 map : Functor f => (m : a -> b) -> f a -> f b

9 The action of the functor on morphisms

10

11+ The function is Total

11Instances:

12Instances:

12 Functor List

13 Functor List

13 Functor Stream

14 Functor Stream

test/docs004/expected+3

@@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a

7

8 baz : Bool -- A field baz

9

10+ The function is Total

10bar : (rec : Foo a) -> Nat

11bar : (rec : Foo a) -> Nat

11 A field bar

12 A field bar

12

13

14+ The function is Total

13baz : (rec : Foo a) -> Bool

15baz : (rec : Foo a) -> Bool

14 A field baz

16 A field baz

15

17

18+ The function is Total

test/interactive005/expected+3

@@ -3,6 +3,7 @@ Hello, World

3main : IO ()

4 This is a docstring

5

6+ The function is Total

6Main.main is Total

7Main.main is Total

7Hello, World

8Hello, World

8Prelude.Basics.id : a -> a

9Prelude.Basics.id : a -> a

@@ -26,8 +27,10 @@ main : IO ()

26 is a

27 is a

27 docstring

28 docstring

28

29

30+ The function is Total

29main : IO ()

31main : IO ()

30 This is a docstring

32 This is a docstring

31

33

34+ The function is Total

32Nat2 : Type

35Nat2 : Type

33Invalid filename for compiler output "Test.idr"

36Invalid filename for compiler output "Test.idr"