cc716d7 · Idris-dev · git.iko.soy

lib/Builtins.idr+7−7

compare with master

unifiedsplit

@@ -1,19 +1,19 @@

1%access public

2%default total

3

4−data Exists : (a : Set) -> (P : a -> Set) -> Set where

4+data Exists : (a : Type) -> (P : a -> Type) -> Type where

5− Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P

5+ Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

6

7−getWitness : {P : a -> Set} -> Exists a P -> a

7+getWitness : {P : a -> Type} -> Exists a P -> a

8getWitness (a ** v) = a

9

10−getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s)

10+getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

11getProof (a ** v) = v

12

13FalseElim : _|_ -> a

14

15-- For rewrite tactic

16−replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y

16+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

17replace refl prf = prf

18

19sym : {l:a} -> {r:a} -> l = r -> r = l

@@ -40,7 +40,7 @@ namespace Builtins {

40id : a -> a

41id x = x

42

43−the : (A : Set) -> A -> A

43+the : (A : Type) -> A -> A

44the _ = id

45

46const : a -> b -> a

@@ -74,7 +74,7 @@ boolElim : Bool -> |(t : a) -> |(f : a) -> a

74boolElim True t e = t

75boolElim False t e = e

76

77−data so : Bool -> Set where oh : so True

77+data so : Bool -> Type where oh : so True

78

79syntax if [test] then [t] else [e] = boolElim test t e

80syntax [test] "?" [t] ":" [e] = if test then t else e

lib/Control/Arrow.idr+1−1

@@ -8,7 +8,7 @@ import Control.Category

8infixr 3 ***

9infixr 3 &&&

10

11−class Category arr => Arrow (arr : Set -> Set -> Set) where

11+class Category arr => Arrow (arr : Type -> Type -> Type) where

12 arrow : (a -> b) -> arr a b

13 first : arr a b -> arr (a, c) (b, c)

14 second : arr a b -> arr (c, a) (c, b)

lib/Control/Category.idr+1−1

@@ -4,7 +4,7 @@ import Data.Morphisms

4

5%access public

6

7−class Category (cat : Set -> Set -> Set) where

7+class Category (cat : Type -> Type -> Type) where

8 id : cat a a

9 (.) : cat b c -> cat a b -> cat a c

10

lib/Control/Monad/Identity.idr+1−1

@@ -4,7 +4,7 @@ import Prelude.Functor

4import Prelude.Applicative

5import Prelude.Monad

6

7−public record Identity : Set -> Set where

7+public record Identity : Type -> Type where

8 Id : (runIdentity : a) -> Identity a

9

10instance Functor Identity where

lib/Control/Monad/State.idr+4−4

@@ -6,12 +6,12 @@ import Prelude.Functor

6

7%access public

8

9−class Monad m => MonadState s (m : Set -> Set) where

9+class Monad m => MonadState s (m : Type -> Type) where

10 get : m s

11 put : s -> m ()

12

13−record StateT : Set -> (Set -> Set) -> Set -> Set where

13+record StateT : Type -> (Type -> Type) -> Type -> Type where

14− ST : {m : Set -> Set} ->

14+ ST : {m : Type -> Type} ->

15 (runStateT : s -> m (a, s)) -> StateT s m a

16

17instance Functor f => Functor (StateT s f) where

@@ -37,6 +37,6 @@ instance Monad m => MonadState s (StateT s m) where

37 get = ST (\x => return (x, x))

38 put x = ST (\y => return ((), x))

39

40−State : Set -> Set -> Set

40+State : Type -> Type -> Type

41State s a = StateT s Identity a

42

lib/Data/Morphisms.idr+4−4

@@ -4,13 +4,13 @@ import Builtins

4

5%access public

6

7−data Homomorphism : Set -> Set -> Set where

7+data Homomorphism : Type -> Type -> Type where

8 Homo : (a -> b) -> Homomorphism a b

9

10−data Endomorphism : Set -> Set where

10+data Endomorphism : Type -> Type where

11 Endo : (a -> a) -> Endomorphism a

12

13−data Kleislimorphism : (Set -> Set) -> Set -> Set -> Set where

13+data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where

14 Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b

15

16applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b

@@ -41,5 +41,5 @@ instance Monoid (Endomorphism a) where

41

42infixr 1 ~>

43

44−(~>) : Set -> Set -> Set

44+(~>) : Type -> Type -> Type

45a ~> b = Homomorphism a b

lib/IO.idr+5−5

@@ -21,9 +21,9 @@ io_return x = prim__IO x

21run__IO : IO () -> IO ()

22run__IO v = io_bind v (\v' => io_return v')

23

25

26−interpFTy : FTy -> Set

26+interpFTy : FTy -> Type

27interpFTy FInt = Int

28interpFTy FFloat = Float

29interpFTy FChar = Char

@@ -32,14 +32,14 @@ interpFTy FPtr = Ptr

32interpFTy (FAny t) = t

33interpFTy FUnit = ()

34

35−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set

35+ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

36ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where

37− mkForeign' : List FTy -> Set -> Set

37+ mkForeign' : List FTy -> Type -> Type

38 mkForeign' Nil ty = ty

39 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)

40

41

42−data Foreign : Set -> Set where

42+data Foreign : Type -> Type where

43 FFun : String -> (xs:List FTy) -> (t:FTy) ->

44 Foreign (ForeignTy xs t)

45

lib/Language/Reflection.idr+1−1

@@ -1,6 +1,6 @@

1module Language.Reflection

2

3−TTName : Set

3+TTName : Type

4TTName = String

5

6data TT = Var TTName

lib/Network/Cgi.idr+3−3

@@ -3,10 +3,10 @@ module Network.Cgi

3import System

4

5public

6−Vars : Set

6+Vars : Type

7Vars = List (String, String)

8

9−record CGIInfo : Set where

9+record CGIInfo : Type where

10 CGISt : (GET : Vars) ->

11 (POST : Vars) ->

12 (Cookies : Vars) ->

@@ -21,7 +21,7 @@ add_Output : String -> CGIInfo -> CGIInfo

21add_Output str st = record { Output = Output st ++ str } st

22

23abstract

24−data CGI : Set -> Set where

24+data CGI : Type -> Type where

25 MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a

26

27getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)

lib/Prelude/Applicative.idr+1−1

@@ -7,7 +7,7 @@ import Prelude.Functor

7

8infixl 2 <$>

9

10−class Functor f => Applicative (f : Set -> Set) where

10+class Functor f => Applicative (f : Type -> Type) where

11 pure : a -> f a

12 (<$>) : f (a -> b) -> f a -> f b

13

lib/Prelude/Fin.idr+1−1

@@ -3,7 +3,7 @@ module Prelude.Fin

3import Prelude.Nat

4import Prelude.Either

5

6−data Fin : Nat -> Set where

6+data Fin : Nat -> Type where

7 fO : Fin (S k)

8 fS : Fin k -> Fin (S k)

9

lib/Prelude/Functor.idr+1−1

@@ -1,4 +1,4 @@

1module Prelude.Functor

2

3−class Functor (f : Set -> Set) where

3+class Functor (f : Type -> Type) where

4 fmap : (a -> b) -> f a -> f b

lib/Prelude/Heap.idr+2−2

@@ -14,7 +14,7 @@ import Prelude.Nat

14

15%access public

16

17−abstract data MaxiphobicHeap : Set -> Set where

17+abstract data MaxiphobicHeap : Type -> Type where

18 Empty : MaxiphobicHeap a

19 Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a

20

@@ -142,7 +142,7 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where

142total absurdBoolDischarge : False = True -> _|_

143absurdBoolDischarge p = replace {P = disjointTy} p ()

144 where

145− total disjointTy : Bool -> Set

145+ total disjointTy : Bool -> Type

146 disjointTy False = ()

147 disjointTy True = _|_

148

lib/Prelude/Monad.idr+2−2

@@ -10,11 +10,11 @@ import Prelude.Applicative

10

11infixl 5 >>=

12

13−class Applicative m => Monad (m : Set -> Set) where

13+class Applicative m => Monad (m : Type -> Type) where

14 return : a -> m a

15 (>>=) : m a -> (a -> m b) -> m b

16

17−class Monad m => MonadPlus (m : Set -> Set) where

17+class Monad m => MonadPlus (m : Type -> Type) where

18 mplus : m a -> m a -> m a

19 mzero : m a

20

lib/Prelude/Nat.idr+6−6

@@ -57,17 +57,17 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

57-- Comparisons

58--------------------------------------------------------------------------------

59

60−data LTE : Nat -> Nat -> Set where

60+data LTE : Nat -> Nat -> Type where

61 lteZero : LTE O right

62 lteSucc : LTE left right -> LTE (S left) (S right)

63

64−total GTE : Nat -> Nat -> Set

64+total GTE : Nat -> Nat -> Type

65GTE left right = LTE right left

66

67−total LT : Nat -> Nat -> Set

67+total LT : Nat -> Nat -> Type

68LT left right = LTE (S left) right

69

70−total GT : Nat -> Nat -> Set

70+total GT : Nat -> Nat -> Type

71GT left right = LT right left

72

73total lte : Nat -> Nat -> Bool

@@ -135,10 +135,10 @@ instance Num Nat where

135 else

136 O

137

138−record Multiplicative : Set where

138+record Multiplicative : Type where

139 getMultiplicative : Nat -> Multiplicative

140

141−record Additive : Set where

141+record Additive : Type where

142 getAdditive : Nat -> Additive

143

144instance Semigroup Multiplicative where

lib/Prelude/Strings.idr+1−1

@@ -8,7 +8,7 @@ import Prelude.Either

8

9-- Some more complex string operations

10

11−data StrM : String -> Set where

11+data StrM : String -> Type where

12 StrNil : StrM ""

13 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

14

lib/Prelude/Vect.idr+1−1

@@ -9,7 +9,7 @@ import Prelude.Nat

9

10infixr 7 ::

11

12−data Vect : Set -> Nat -> Set where

12+data Vect : Type -> Nat -> Type where

13 Nil : Vect a O

14 (::) : a -> Vect a n -> Vect a (S n)

15

lib/System/Concurrency/Process.idr+1−1

@@ -12,7 +12,7 @@ data ProcID msg = MkPID Ptr

12-- Type safe message passing programs. Parameterised over the type of

13-- message which can be send, and the return type.

14

15−data Process : (msgType : Set) -> Set -> Set where

15+data Process : (msgType : Type) -> Type -> Type where

16 lift : IO a -> Process msg a

17

18instance Functor (Process msg) where

src/Core/CoreParser.hs+1−1

@@ -28,7 +28,7 @@ idrisDef = haskellDef {

28 reservedOpNames

29 = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

30 reservedNames

31− = ["let", "in", "data", "codata", "record", "Set",

31+ = ["let", "in", "data", "codata", "record", "Type",

32 "do", "dsl", "import", "impossible",

33 "case", "of", "total", "partial", "mutual",

34 "infix", "infixl", "infixr",

src/Idris/Parser.hs+1−1

@@ -760,7 +760,7 @@ pSimpleExpr syn =

760 <|> try (do c <- pConstant

761 fc <- pfc

762 return (modifyConst syn fc (PConstant c)))

763− <|> do reserved "Set"; return PSet

763+ <|> do reserved "Type"; return PSet

764 <|> try (do symbol "()"

765 fc <- pfc

766 return (PTrue fc))

test/reg001/reg001.idr+3−3

@@ -1,11 +1,11 @@

1apply : (a -> b) -> a -> b

2apply f x = f x

3

4−class Functor f => VerifiedFunctor (f : Set -> Set) where

4+class Functor f => VerifiedFunctor (f : Type -> Type) where

5 identity : (fa : f a) -> fmap id fa = fa

6

7−data Imp : Set where

7+data Imp : Type where

8− MkImp : {any : Set} -> any -> Imp

8+ MkImp : {any : Type} -> any -> Imp

9

10testVal : Imp

11testVal = MkImp (apply id O)

test/reg003/reg003.idr+2−2

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

1

2mutual

3 namespace Even

4− data EvenList : Set where

4+ data EvenList : Type where

5 Nil : EvenList

6 (::) : Nat -> OddList -> EvenList

7

8 namespace Odd

9− data OddList : Set where

9+ data OddList : Type where

10 (::) : Nat -> EvenList -> OddList

11

12test : EvenList

test/reg003/reg003a.idr+2−2

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

1

2−data EvenList : Set where

2+data EvenList : Type where

3 ENil : EvenList

4 ECons : Nat -> OddList -> EvenList

5

6−data OddList : Set where

6+data OddList : Type where

7 OCons : Nat -> EvenList -> OddList

8

9test : EvenList

test/reg005/reg005.idr+1−1

@@ -4,7 +4,7 @@ rep : (n : Nat) -> Char -> Vect Char n

4rep O x = []

5rep (S k) x = x :: rep k x

6

7−data RLE : Vect Char n -> Set where

7+data RLE : Vect Char n -> Type where

8 REnd : RLE []

9 RChar : {xs : Vect Char k} ->

10 (n : Nat) -> (x : Char) -> RLE xs ->

test/test001/test001.idr+4−4

@@ -2,18 +2,18 @@ module Main

2

3data Ty = TyInt | TyBool| TyFun Ty Ty

4

5−interpTy : Ty -> Set

5+interpTy : Ty -> Type

6interpTy TyInt = Int

7interpTy TyBool = Bool

8interpTy (TyFun s t) = interpTy s -> interpTy t

9

10using (G : Vect Ty n)

11

12− data Env : Vect Ty n -> Set where

12+ data Env : Vect Ty n -> Type where

13 Nil : Env Nil

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

17 stop : HasType fO (t :: G) t

18 pop : HasType k G t -> HasType (fS k) (u :: G) t

19

@@ -22,7 +22,7 @@ using (G : Vect Ty n)

22 lookup (pop k) (x :: xs) = lookup k xs

23 lookup stop [] impossible

24

25− data Expr : Vect Ty n -> Ty -> Set where

25+ data Expr : Vect Ty n -> Ty -> Type where

26 Var : HasType i G t -> Expr G t

27 Val : (x : Int) -> Expr G TyInt

28 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

test/test002/test002.idr+5−5

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

1myid : a -> a

2myid x = x

3

4−idid : (a : Set) -> a -> a

4+idid : (a : Type) -> a -> a

5idid = myid ![myid]

6

7app : (a -> b) -> a -> b

@@ -15,14 +15,14 @@ doapp x = app myid x

15

16{-

17

18−id : (b : Set k) -> b -> b : Set l, k < l

18+id : (b : Type k) -> b -> b : Type l, k < l

19

20−foo = id ((a : Set k) -> a -> a) id

20+foo = id ((a : Type k) -> a -> a) id

21− Set m, k < m

21+ Type m, k < m

22

23So we have k < m, k < l, m <= k

24

25− when converting Set m against Set n, we must have m <= n

25+ when converting Type m against Type n, we must have m <= n

26 if we can reach m from n, we have an inconsistency

27

28

test/test006/test006.idr+1−1

@@ -1,6 +1,6 @@

1module Main

2

3−data Parity : Nat -> Set where

3+data Parity : Nat -> Type where

4 even : Parity (n + n)

5 odd : Parity (S (n + n))

6

test/test007/test007.idr+1−1

@@ -4,7 +4,7 @@ data Expr = Var String

4 | Val Int

5 | Add Expr Expr

6

7−data Eval : Set -> Set where

7+data Eval : Type -> Type where

8 MkEval : (List (String, Int) -> Maybe a) -> Eval a

9

10fetch : String -> Eval Int

test/test011/test011.idr+2−2

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

1module Main

2

3−record Foo : Nat -> Set where

3+record Foo : Nat -> Type where

4 MkFoo : (name : String) ->

5 (things : Vect a n) ->

6 (more_things : Vect b m) ->

7 Foo n

8

9−record Person : Set where

9+record Person : Type where

10 MkPerson : (name : String) -> (age : Int) -> Person

11

12testFoo : Foo 3

test/test014/Resimp.idr+13−13

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

1module Resimp

2

3-- IO operations which read a resource

4−data Reader : Set -> Set where

4+data Reader : Type -> Type where

5 MkReader : IO a -> Reader a

6

7getReader : Reader a -> IO a

@@ -11,7 +11,7 @@ ior : IO a -> Reader a

11ior = MkReader

12

13-- IO operations which update a resource

14−data Updater : Set -> Set where

14+data Updater : Type -> Type where

15 MkUpdater : IO a -> Updater a

16

17getUpdater : Updater a -> IO a

@@ -21,7 +21,7 @@ iou : IO a -> Updater a

21iou = MkUpdater

22

23-- IO operations which create a resource

24−data Creator : Set -> Set where

24+data Creator : Type -> Type where

25 MkCreator : IO a -> Creator a

26

27getCreator : Creator a -> IO a

@@ -34,22 +34,22 @@ infixr 5 :->

34

35using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

36

37− data Ty = R Set

37+ data Ty = R Type

38− | Val Set

38+ | Val Type

39− | Choice Set Set

39+ | Choice Type Type

40− | (:->) Set Ty

40+ | (:->) Type Ty

41

42− interpTy : Ty -> Set

42+ interpTy : Ty -> Type

43 interpTy (R t) = IO t

44 interpTy (Val t) = t

45 interpTy (Choice x y) = Either x y

46 interpTy (a :-> b) = a -> interpTy b

47

48− data HasType : Vect Ty n -> Fin n -> Ty -> Set where

48+ data HasType : Vect Ty n -> Fin n -> Ty -> Type where

49 stop : HasType (a :: gam) fO a

50 pop : HasType gam i b -> HasType (a :: gam) (fS i) b

51

52− data Env : Vect Ty n -> Set where

52+ data Env : Vect Ty n -> Type where

53 Nil : Env Nil

54 (::) : interpTy a -> Env gam -> Env (a :: gam)

55

@@ -72,16 +72,16 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

72 envTail : Env (a :: gam) -> Env gam

73 envTail (x :: xs) = xs

74

75− data Args : Vect Ty n -> List Set -> Set where

75+ data Args : Vect Ty n -> List Type -> Type where

76 ANil : Args gam []

77 ACons : HasType gam i a ->

78 Args gam as -> Args gam (interpTy a :: as)

79

80− funTy : List Set -> Ty -> Ty

80+ funTy : List Type -> Ty -> Ty

81 funTy list.Nil t = t

82 funTy (a :: as) t = a :-> funTy as t

83

84− data Res : Vect Ty n -> Vect Ty n -> Ty -> Set where

84+ data Res : Vect Ty n -> Vect Ty n -> Ty -> Type where

85

86{-- Resource creation and usage. 'Let' creates a resource - the type

87 at the end means that the resource must have been consumed by the time

test/test014/test014.idr+1−1

@@ -8,7 +8,7 @@ pstring : Purpose -> String

8pstring Reading = "r"

9pstring Writing = "w"

10

11−data FILE : Purpose -> Set where

11+data FILE : Purpose -> Type where

12 OpenH : File -> FILE p

13

14syntax ifM [test] then [t] else [e]

test/test015/Parity.idr+1−1

@@ -1,6 +1,6 @@

1module Parity

2

3−data Parity : Nat -> Set where

3+data Parity : Nat -> Type where

4 even : Parity (n + n)

5 odd : Parity (S (n + n))

6

test/test015/test015.idr+2−2

@@ -3,7 +3,7 @@ module Main

3import Parity

4import System

5

6−data Bit : Nat -> Set where

6+data Bit : Nat -> Type where

7 b0 : Bit O

8 b1 : Bit (S O)

9

@@ -15,7 +15,7 @@ instance Show (Bit n) where

15

16infixl 5 #

17

18−data Binary : (width : Nat) -> (value : Nat) -> Set where

18+data Binary : (width : Nat) -> (value : Nat) -> Type where

19 zero : Binary O O

20 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

21

test/test017/test017.idr+2−2

@@ -4,13 +4,13 @@ module scg

4

5data Ord = Zero | Suc Ord | Sup (Nat -> Ord)

6

7−natElim : (n : Nat) -> (P : Nat -> Set) ->

7+natElim : (n : Nat) -> (P : Nat -> Type) ->

8 (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)

9natElim O P mO mS = mO

10natElim (S k) P mO mS = mS k (natElim k P mO mS)

11

12ordElim : (x : Ord) ->

13− (P : Ord -> Set) ->

13+ (P : Ord -> Type) ->

14 (P Zero) ->

15 ((x : Ord) -> P x -> P (Suc x)) ->

16 ((f : Nat -> Ord) -> ((n : Nat) -> P (f n)) ->

tutorial/classes.tex+6−6

@@ -195,14 +195,14 @@ sortAndShow xs = show (sort xs)

195\label{sec:monad}

196

197So far, we have seen single parameter type classes, where the parameter is of type

198−\texttt{Set}. In general, there can be any number (greater than 0) of parameters,

198+\texttt{Type}. In general, there can be any number (greater than 0) of parameters,

199and the parameters can have \remph{any} type.

200−If the type of the parameter is not \texttt{Set}, we need to give an explicit type

200+If the type of the parameter is not \texttt{Type}, we need to give an explicit type

201declaration. For example:

202

203\begin{SaveVerbatim}{monad}

204

205−class Monad (m : Set -> Set) where

205+class Monad (m : Type -> Type) where

206 return : a -> m a

207 (>>=) : m a -> (a -> m b) -> m b

208

@@ -272,7 +272,7 @@ general, and applies to anything which is an instance of \texttt{MonadPlus}:

272

273\begin{SaveVerbatim}{monadplus}

274

275−class Monad m => MonadPlus (m : Set -> Set) where

275+class Monad m => MonadPlus (m : Type -> Type) where

276 mplus : m a -> m a -> m a

277 mzero : m a

278

@@ -363,7 +363,7 @@ class, which captures the notion of application for a data type:

363

364infixl 2 <$>

365

366−class Applicative (f : Set -> Set) where

366+class Applicative (f : Type -> Type) where

367 pure : a -> f a

368 (<$>) : f (a -> b) -> f a -> f b

369

@@ -420,7 +420,7 @@ Evaluation will take place relative to a context mapping variables (represented

420

421\begin{SaveVerbatim}{evalctxt}

422

423−data Eval : Set -> Set where

423+data Eval : Type -> Type where

424 MkEval : (List (String, Int) -> Maybe a) -> Eval a

425

426\end{SaveVerbatim}

tutorial/examples/binary.idr+2−2

@@ -1,6 +1,6 @@

1module Main

2

3−data Binary : Nat -> Set where

3+data Binary : Nat -> Type where

4 bEnd : Binary O

5 bO : Binary n -> Binary (n + n)

6 bI : Binary n -> Binary (S (n + n))

@@ -12,7 +12,7 @@ instance Show (Binary n) where

12 show' (bI x) = show x ++ "1"

13 show' bEnd = ""

14

15−data Parity : Nat -> Set where

15+data Parity : Nat -> Type where

16 even : Parity (n + n)

17 odd : Parity (S (n + n))

18

tutorial/examples/idiom.idr+1−1

@@ -4,7 +4,7 @@ data Expr = Var String

4 | Val Int

5 | Add Expr Expr

6

7−data Eval : Set -> Set where

7+data Eval : Type -> Type where

8 MkEval : (List (String, Int) -> Maybe a) -> Eval a

9

10fetch : String -> Eval Int

tutorial/examples/interp.idr+4−4

@@ -2,18 +2,18 @@ module Main

2

3data Ty = TyInt | TyBool| TyFun Ty Ty

4

5−interpTy : Ty -> Set

5+interpTy : Ty -> Type

6interpTy TyInt = Int

7interpTy TyBool = Bool

8interpTy (TyFun s t) = interpTy s -> interpTy t

9

10using (G : Vect Ty n)

11

12− data Env : Vect Ty n -> Set where

12+ data Env : Vect Ty n -> Type where

13 Nil : Env Nil

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

17 stop : HasType fO (t :: G) t

18 pop : HasType k G t -> HasType (fS k) (u :: G) t

19

@@ -21,7 +21,7 @@ using (G : Vect Ty n)

21 lookup stop (x :: xs) = x

22 lookup (pop k) (x :: xs) = lookup k xs

23

24− data Expr : Vect Ty n -> Ty -> Set where

24+ data Expr : Vect Ty n -> Ty -> Type where

25 Var : HasType i G t -> Expr G t

26 Val : (x : Int) -> Expr G TyInt

27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

tutorial/examples/theorems.idr+1−1

@@ -8,7 +8,7 @@ twoPlusTwo = refl

8total disjoint : (n : Nat) -> O = S n -> _|_

9disjoint n p = replace {P = disjointTy} p ()

10 where

11− disjointTy : Nat -> Set

11+ disjointTy : Nat -> Type

12 disjointTy O = ()

13 disjointTy (S k) = _|_

14

tutorial/examples/universe.idr+2−2

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

1−myid : (a : Set) -> a -> a

1+myid : (a : Type) -> a -> a

2myid _ x = x

3

4−idid : (a : Set) -> a -> a

4+idid : (a : Type) -> a -> a

5idid = myid _ myid

6

7

tutorial/examples/views.idr+1−1

@@ -1,6 +1,6 @@

1module views

2

3−data Parity : Nat -> Set where

3+data Parity : Nat -> Type where

4 even : Parity (n + n)

5 odd : Parity (S (n + n))

6

tutorial/interp.tex+6−6

@@ -23,7 +23,7 @@ any other value:

23

24\begin{SaveVerbatim}{interpty}

25

26−interpTy : Ty -> Set

26+interpTy : Ty -> Type

27interpTy TyInt = Int

28interpTy TyBool = Bool

29interpTy (TyFun A T) = interpTy A -> interpTy T

@@ -51,7 +51,7 @@ indexed by the types of the local variables, and the type of the expression itse

51

52\begin{SaveVerbatim}{exprdecl}

53

54−data Expr : Vect Ty n -> Ty -> Set

54+data Expr : Vect Ty n -> Ty -> Type

55

56\end{SaveVerbatim}

57\useverb{exprdecl}

@@ -63,11 +63,11 @@ constructor in turn.

63

64\begin{SaveVerbatim}{exprty}

65

66−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

66+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

67 stop : HasType fO (t :: G) t

68 pop : HasType k G t -> HasType (fS k) (u :: G) t

69

70−data Expr : Vect Ty n -> Ty -> Set where

70+data Expr : Vect Ty n -> Ty -> Type where

71 Var : HasType i G t -> Expr G t

72 Val : (x : Int) -> Expr G TyInt

73 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

@@ -87,7 +87,7 @@ Variables are represented by a proof of their membership in the context,

87

88\begin{SaveVerbatim}{hastype}

89

90−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

90+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

91 stop : HasType fO (t :: G) t

92 pop : HasType k G t -> HasType (fS k) (u :: G) t

93

@@ -181,7 +181,7 @@ is defined in the context, we can then produce a value from the environment:

181

182\begin{SaveVerbatim}{envtype}

183

184−data Env : Vect Ty n -> Set where

184+data Env : Vect Ty n -> Type where

185 Nil : Env Nil

186 (::) : interpTy a -> Env G -> Env (a :: G)

187

tutorial/miscellany.tex+17−17

@@ -120,7 +120,7 @@ following function:

120

121\begin{SaveVerbatim}{interpfty}

122

123−interpFTy : FTy -> Set

123+interpFTy : FTy -> Type

124interpFTy FInt = Int

125interpFTy FFloat = Float

126interpFTy FChar = Char

@@ -137,7 +137,7 @@ can then be converted to an \Idris{} type:

137

138\begin{SaveVerbatim}{ffunty}

139

140−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set

140+ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

141

142\end{SaveVerbatim}

143\useverb{ffunty}

@@ -149,10 +149,10 @@ A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an

149\begin{SaveVerbatim}{ftyex}

150

151Idris> ForeignTy [FInt, FString] FString

152−Int -> String -> IO String : Set

152+Int -> String -> IO String : Type

153

154Idris> ForeignTy [FInt, FString] FUnit

155−Int -> String -> IO () : Set

155+Int -> String -> IO () : Type

156

157\end{SaveVerbatim}

158\useverb{ftyex}

@@ -164,7 +164,7 @@ converts this description to a function callable by \Idris{}

164

165\begin{SaveVerbatim}{mkForeign}

166

167−data Foreign : Set -> Set where

167+data Foreign : Type -> Type where

168 FFun : String -> (xs:List FTy) -> (t:FTy) ->

169 Foreign (ForeignTy xs t)

170

@@ -206,39 +206,39 @@ have types. For example:

206\begin{SaveVerbatim}{typetypes}

207

208*universe> :t Nat

209−Nat : Set

209+Nat : Type

210*universe> :t Vect

211−Vect : Set -> Nat -> Set

211+Vect : Type -> Nat -> Type

212

213\end{SaveVerbatim}

214\useverb{typetypes}

215

216\noindent

217−But what about the type of \texttt{Set}? If we ask \Idris{} it reports

217+But what about the type of \texttt{Type}? If we ask \Idris{} it reports

218

219\begin{SaveVerbatim}{setset}

220

221−*universe> :t Set

221+*universe> :t Type

222−Set : Set

222+Type : Type

223

224\end{SaveVerbatim}

225\useverb{setset}

226

227\noindent

228−It \emph{appears} that \texttt{Set} is its own type. This would lead to an inconsitency

228+It \emph{appears} that \texttt{Type} is its own type. This would lead to an inconsitency

229due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}

230of types (or \emph{universes}):

231

232\begin{SaveVerbatim}{sethierarchy}

233

234−Set : Set 1 : Set 2 : Set 3 : ...

234+Type : Type 1 : Type 2 : Type 3 : ...

235

236\end{SaveVerbatim}

237\useverb{sethierarchy}

238

239\noindent

240−Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that

240+Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that

241−\texttt{x : Set m}, as long as \texttt{n < m}.

241+\texttt{x : Type m}, as long as \texttt{n < m}.

242The typechecker generates such universe

243constraints and reports an error if any inconsistencies are found. Ordinarily, a

244programmer does not need to worry about this, but it does prevent (contrived)

@@ -246,10 +246,10 @@ programs such as the following:

246

247\begin{SaveVerbatim}{idid}

248

249−myid : (a : Set) -> a -> a

249+myid : (a : Type) -> a -> a

250myid _ x = x

251

252−idid : (a : Set) -> a -> a

252+idid : (a : Type) -> a -> a

253idid = myid _ myid

254

255\end{SaveVerbatim}

@@ -257,7 +257,7 @@ idid = myid _ myid

257

258\noindent

259The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy

260−--- \texttt{myid}'s first argument is a \texttt{Set}, which cannot be at a lower level

260+--- \texttt{myid}'s first argument is a \texttt{Type}, which cannot be at a lower level

261than required if it is applied to itself.

262

263%\subsection{Comparison}

tutorial/modules.tex+1−1

@@ -208,7 +208,7 @@ constructors. They may also be dependent types with implicit arguments:

208\begin{SaveVerbatim}{paramdata}

209

210parameters (xs : Vect a x, y : Nat)

211− data Vects : Set -> Set where

211+ data Vects : Type -> Type where

212 MkVects : Vect a y -> Vects a

213

214 append : Vects a -> Vect a (x + y)

tutorial/provisional.tex+2−2

@@ -7,7 +7,7 @@ example, recall the \texttt{parity} function:

7

8\begin{SaveVerbatim}{pardecl}

9

10−data Parity : Nat -> Set where

10+data Parity : Nat -> Type where

11 even : Parity (n + n)

12 odd : Parity (S (n + n))

13

@@ -230,7 +230,7 @@ case \texttt{Nat}):

230

231\begin{SaveVerbatim}{bindef}

232

233−data Binary : Nat -> Set where

233+data Binary : Nat -> Type where

234 bEnd : Binary O

235 bO : Binary n -> Binary (n + n)

236 bI : Binary n -> Binary (S (n + n))

tutorial/syntax.tex+1−1

@@ -72,7 +72,7 @@ that the lower bound is below the upper bound using \texttt{so}:

72

73\begin{SaveVerbatim}{interval}

74

75−data Interval : Set where

75+data Interval : Type where

76 MkInterval : (lower : Float) -> (upper : Float) ->

77 so (lower < upper) -> Interval

78

tutorial/theorems.tex+2−2

@@ -8,7 +8,7 @@ the following definition:

8

9\begin{SaveVerbatim}{}

10

11−data (=) : a -> b -> Set where

11+data (=) : a -> b -> Type where

12 refl : x = x

13

14\end{SaveVerbatim}

@@ -45,7 +45,7 @@ to a successor:

45disjoint : (n : Nat) -> O = S n -> _|_

46disjoint n p = replace {P = disjointTy} p ()

47 where

48− disjointTy : Nat -> Set

48+ disjointTy : Nat -> Type

49 disjointTy O = ()

50 disjointTy (S k) = _|_

51

tutorial/typesfuns.tex+12−12

@@ -289,7 +289,7 @@ we declare vectors as follows:

289

290\begin{SaveVerbatim}{vect}

291

292−data Vect : Set -> Nat -> Set where

292+data Vect : Type -> Nat -> Type where

293 Nil : Vect a O

294 (::) : a -> Vect a k -> Vect a (S k)

295

@@ -305,7 +305,7 @@ Ambiguous constructor names can normally be resolved from context.

305This declares a family of types, and so the form of the declaration is rather

306different from the simple type declarations above. We explicitly state the type

307of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

308−argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}

308+argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

309is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

310constructor targets a different part of the family of types. \tDC{Nil} can only

311be used to construct vectors with zero length, and \tDC{::} to construct

@@ -370,7 +370,7 @@ They are declared as follows (again, in the prelude):

370

371\begin{SaveVerbatim}{findecl}

372

373−data Fin : Nat -> Set where

373+data Fin : Nat -> Type where

374 fO : Fin (S k)

375 fS : Fin k -> Fin (S k)

376

@@ -433,7 +433,7 @@ arguments to \texttt{index}. We could also write the type of \texttt{index} as:

433

434\begin{SaveVerbatim}{vindeximpty}

435

436−index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a

436+index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

437

438\end{SaveVerbatim}

439\useverb{vindeximpty}

@@ -481,7 +481,7 @@ definition, which defines a predicate on vectors:

481

482\begin{SaveVerbatim}{elem}

483

484−data Elem : a -> Vect a n -> Set where

484+data Elem : a -> Vect a n -> Type where

485 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

486 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

487

@@ -513,7 +513,7 @@ ordering of any implicit arguments which can appear within the block:

513\begin{SaveVerbatim}{elemusing}

514

515using (x:a, y:a, xs:Vect a n)

516− data Elem : a -> Vect a n -> Set where

516+ data Elem : a -> Vect a n -> Type where

517 here : Elem x (x :: xs)

518 there : Elem x xs -> Elem x (y :: xs)

519

@@ -674,7 +674,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:

674

675data List a = Nil | (::) a (List a)

676

677−data Vect : Set -> Nat -> Set where

677+data Vect : Type -> Nat -> Type where

678 Nil : Vect a O

679 (::) : a -> Vect a k -> Vect a (S k)

680

@@ -858,8 +858,8 @@ the value of the first element:

858

859\begin{SaveVerbatim}{sigma}

860

861−data Exists : (A : Set) -> (P : A -> Set) -> Set where

861+data Exists : (A : Type) -> (P : A -> Type) -> Type where

862− Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P

862+ Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P

863

864\end{SaveVerbatim}

865\useverb{sigma}

@@ -951,7 +951,7 @@ value is true:

951

952\begin{SaveVerbatim}{sotype}

953

954−data so : Bool -> Set where

954+data so : Bool -> Type where

955 oh : so True

956

957\end{SaveVerbatim}

@@ -1112,7 +1112,7 @@ can represent a person's name and age in a record:

1112

1113\begin{SaveVerbatim}{recsimpl}

1114

1115−record Person : Set where

1115+record Person : Type where

1116 MkPerson : (name : String) ->

1117 (age : Int) -> Person

1118

@@ -1165,7 +1165,7 @@ the record as a whole. For example:

1165

1166\begin{SaveVerbatim}{deprec}

1167

1168−record Class : Set where

1168+record Class : Type where

1169 ClassInfo : (students : Vect Person n) ->

1170 (className : String) ->

1171 Class

tutorial/views.tex+1−1

@@ -56,7 +56,7 @@ plus one:

56

57\begin{SaveVerbatim}{parity}

58

59−data Parity : Nat -> Set where

59+data Parity : Nat -> Type where

60 even : Parity (n + n)

61 odd : Parity (S (n + n))

62