git.iko.soy/Idris-dev
on master help sign in
Make 'Type' the type of types instead of Sets

...after mailing list discussion

commitcc716d788475b0970a128cf35874b743869a03fe authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 11 Dec 2012, 23:02 (14 years ago) parentbdf11e8
49 files changed+144−144
compare with master
unifiedsplit
lib/Builtins.idr+7−7 lib/Control/Arrow.idr+1−1 lib/Control/Category.idr+1−1 lib/Control/Monad/Identity.idr+1−1 lib/Control/Monad/State.idr+4−4 lib/Data/Morphisms.idr+4−4 lib/IO.idr+5−5 lib/Language/Reflection.idr+1−1 lib/Network/Cgi.idr+3−3 lib/Prelude/Applicative.idr+1−1 lib/Prelude/Fin.idr+1−1 lib/Prelude/Functor.idr+1−1 lib/Prelude/Heap.idr+2−2 lib/Prelude/Monad.idr+2−2 lib/Prelude/Nat.idr+6−6 lib/Prelude/Strings.idr+1−1 lib/Prelude/Vect.idr+1−1 lib/System/Concurrency/Process.idr+1−1 src/Core/CoreParser.hs+1−1 src/Idris/Parser.hs+1−1 test/reg001/reg001.idr+3−3 test/reg003/reg003.idr+2−2 test/reg003/reg003a.idr+2−2 test/reg005/reg005.idr+1−1 test/test001/test001.idr+4−4 test/test002/test002.idr+5−5 test/test006/test006.idr+1−1 test/test007/test007.idr+1−1 test/test011/test011.idr+2−2 test/test014/Resimp.idr+13−13 test/test014/test014.idr+1−1 test/test015/Parity.idr+1−1 test/test015/test015.idr+2−2 test/test017/test017.idr+2−2 tutorial/classes.tex+6−6 tutorial/examples/binary.idr+2−2 tutorial/examples/idiom.idr+1−1 tutorial/examples/interp.idr+4−4 tutorial/examples/theorems.idr+1−1 tutorial/examples/universe.idr+2−2 tutorial/examples/views.idr+1−1 tutorial/interp.tex+6−6 tutorial/miscellany.tex+17−17 tutorial/modules.tex+1−1 tutorial/provisional.tex+2−2 tutorial/syntax.tex+1−1 tutorial/theorems.tex+2−2 tutorial/typesfuns.tex+12−12 tutorial/views.tex+1−1
lib/Builtins.idr+7−7
@@ -1,19 +1,19 @@
11%access public
22%default total
33
4−data Exists : (a : Set) -> (P : a -> Set) -> Set where
5− Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P
4+data Exists : (a : Type) -> (P : a -> Type) -> Type where
5+ Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P
66
7−getWitness : {P : a -> Set} -> Exists a P -> a
7+getWitness : {P : a -> Type} -> Exists a P -> a
88getWitness (a ** v) = a
99
10−getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s)
10+getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
1111getProof (a ** v) = v
1212
1313FalseElim : _|_ -> a
1414
1515-- 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
1717replace refl prf = prf
1818
1919sym : {l:a} -> {r:a} -> l = r -> r = l
@@ -40,7 +40,7 @@ namespace Builtins {
4040id : a -> a
4141id x = x
4242
43−the : (A : Set) -> A -> A
43+the : (A : Type) -> A -> A
4444the _ = id
4545
4646const : a -> b -> a
@@ -74,7 +74,7 @@ boolElim : Bool -> |(t : a) -> |(f : a) -> a
7474boolElim True t e = t
7575boolElim False t e = e
7676
77−data so : Bool -> Set where oh : so True
77+data so : Bool -> Type where oh : so True
7878
7979syntax if [test] then [t] else [e] = boolElim test t e
8080syntax [test] "?" [t] ":" [e] = if test then t else e
lib/Control/Arrow.idr+1−1
@@ -8,7 +8,7 @@ import Control.Category
88infixr 3 ***
99infixr 3 &&&
1010
11−class Category arr => Arrow (arr : Set -> Set -> Set) where
11+class Category arr => Arrow (arr : Type -> Type -> Type) where
1212 arrow : (a -> b) -> arr a b
1313 first : arr a b -> arr (a, c) (b, c)
1414 second : arr a b -> arr (c, a) (c, b)
lib/Control/Category.idr+1−1
@@ -4,7 +4,7 @@ import Data.Morphisms
44
55%access public
66
7−class Category (cat : Set -> Set -> Set) where
7+class Category (cat : Type -> Type -> Type) where
88 id : cat a a
99 (.) : cat b c -> cat a b -> cat a c
1010
lib/Control/Monad/Identity.idr+1−1
@@ -4,7 +4,7 @@ import Prelude.Functor
44import Prelude.Applicative
55import Prelude.Monad
66
7−public record Identity : Set -> Set where
7+public record Identity : Type -> Type where
88 Id : (runIdentity : a) -> Identity a
99
1010instance Functor Identity where
lib/Control/Monad/State.idr+4−4
@@ -6,12 +6,12 @@ import Prelude.Functor
66
77%access public
88
9−class Monad m => MonadState s (m : Set -> Set) where
9+class Monad m => MonadState s (m : Type -> Type) where
1010 get : m s
1111 put : s -> m ()
1212
13−record StateT : Set -> (Set -> Set) -> Set -> Set where
14− ST : {m : Set -> Set} ->
13+record StateT : Type -> (Type -> Type) -> Type -> Type where
14+ ST : {m : Type -> Type} ->
1515 (runStateT : s -> m (a, s)) -> StateT s m a
1616
1717instance Functor f => Functor (StateT s f) where
@@ -37,6 +37,6 @@ instance Monad m => MonadState s (StateT s m) where
3737 get = ST (\x => return (x, x))
3838 put x = ST (\y => return ((), x))
3939
40−State : Set -> Set -> Set
40+State : Type -> Type -> Type
4141State s a = StateT s Identity a
4242
lib/Data/Morphisms.idr+4−4
@@ -4,13 +4,13 @@ import Builtins
44
55%access public
66
7−data Homomorphism : Set -> Set -> Set where
7+data Homomorphism : Type -> Type -> Type where
88 Homo : (a -> b) -> Homomorphism a b
99
10−data Endomorphism : Set -> Set where
10+data Endomorphism : Type -> Type where
1111 Endo : (a -> a) -> Endomorphism a
1212
13−data Kleislimorphism : (Set -> Set) -> Set -> Set -> Set where
13+data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
1414 Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
1515
1616applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
@@ -41,5 +41,5 @@ instance Monoid (Endomorphism a) where
4141
4242infixr 1 ~>
4343
44−(~>) : Set -> Set -> Set
44+(~>) : Type -> Type -> Type
4545a ~> b = Homomorphism a b
lib/IO.idr+5−5
@@ -21,9 +21,9 @@ io_return x = prim__IO x
2121run__IO : IO () -> IO ()
2222run__IO v = io_bind v (\v' => io_return v')
2323
24−data FTy = FInt | FFloat | FChar | FString | FPtr | FAny Set | FUnit
24+data FTy = FInt | FFloat | FChar | FString | FPtr | FAny Type | FUnit
2525
26−interpFTy : FTy -> Set
26+interpFTy : FTy -> Type
2727interpFTy FInt = Int
2828interpFTy FFloat = Float
2929interpFTy FChar = Char
@@ -32,14 +32,14 @@ interpFTy FPtr = Ptr
3232interpFTy (FAny t) = t
3333interpFTy FUnit = ()
3434
35−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
35+ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
3636ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where
37− mkForeign' : List FTy -> Set -> Set
37+ mkForeign' : List FTy -> Type -> Type
3838 mkForeign' Nil ty = ty
3939 mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
4040
4141
42−data Foreign : Set -> Set where
42+data Foreign : Type -> Type where
4343 FFun : String -> (xs:List FTy) -> (t:FTy) ->
4444 Foreign (ForeignTy xs t)
4545
lib/Language/Reflection.idr+1−1
@@ -1,6 +1,6 @@
11module Language.Reflection
22
3−TTName : Set
3+TTName : Type
44TTName = String
55
66data TT = Var TTName
lib/Network/Cgi.idr+3−3
@@ -3,10 +3,10 @@ module Network.Cgi
33import System
44
55public
6−Vars : Set
6+Vars : Type
77Vars = List (String, String)
88
9−record CGIInfo : Set where
9+record CGIInfo : Type where
1010 CGISt : (GET : Vars) ->
1111 (POST : Vars) ->
1212 (Cookies : Vars) ->
@@ -21,7 +21,7 @@ add_Output : String -> CGIInfo -> CGIInfo
2121add_Output str st = record { Output = Output st ++ str } st
2222
2323abstract
24−data CGI : Set -> Set where
24+data CGI : Type -> Type where
2525 MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a
2626
2727getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
lib/Prelude/Applicative.idr+1−1
@@ -7,7 +7,7 @@ import Prelude.Functor
77
88infixl 2 <$>
99
10−class Functor f => Applicative (f : Set -> Set) where
10+class Functor f => Applicative (f : Type -> Type) where
1111 pure : a -> f a
1212 (<$>) : f (a -> b) -> f a -> f b
1313
lib/Prelude/Fin.idr+1−1
@@ -3,7 +3,7 @@ module Prelude.Fin
33import Prelude.Nat
44import Prelude.Either
55
6−data Fin : Nat -> Set where
6+data Fin : Nat -> Type where
77 fO : Fin (S k)
88 fS : Fin k -> Fin (S k)
99
lib/Prelude/Functor.idr+1−1
@@ -1,4 +1,4 @@
11module Prelude.Functor
22
3−class Functor (f : Set -> Set) where
3+class Functor (f : Type -> Type) where
44 fmap : (a -> b) -> f a -> f b
lib/Prelude/Heap.idr+2−2
@@ -14,7 +14,7 @@ import Prelude.Nat
1414
1515%access public
1616
17−abstract data MaxiphobicHeap : Set -> Set where
17+abstract data MaxiphobicHeap : Type -> Type where
1818 Empty : MaxiphobicHeap a
1919 Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a
2020
@@ -142,7 +142,7 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
142142total absurdBoolDischarge : False = True -> _|_
143143absurdBoolDischarge p = replace {P = disjointTy} p ()
144144 where
145− total disjointTy : Bool -> Set
145+ total disjointTy : Bool -> Type
146146 disjointTy False = ()
147147 disjointTy True = _|_
148148
lib/Prelude/Monad.idr+2−2
@@ -10,11 +10,11 @@ import Prelude.Applicative
1010
1111infixl 5 >>=
1212
13−class Applicative m => Monad (m : Set -> Set) where
13+class Applicative m => Monad (m : Type -> Type) where
1414 return : a -> m a
1515 (>>=) : m a -> (a -> m b) -> m b
1616
17−class Monad m => MonadPlus (m : Set -> Set) where
17+class Monad m => MonadPlus (m : Type -> Type) where
1818 mplus : m a -> m a -> m a
1919 mzero : m a
2020
lib/Prelude/Nat.idr+6−6
@@ -57,17 +57,17 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
5757-- Comparisons
5858--------------------------------------------------------------------------------
5959
60−data LTE : Nat -> Nat -> Set where
60+data LTE : Nat -> Nat -> Type where
6161 lteZero : LTE O right
6262 lteSucc : LTE left right -> LTE (S left) (S right)
6363
64−total GTE : Nat -> Nat -> Set
64+total GTE : Nat -> Nat -> Type
6565GTE left right = LTE right left
6666
67−total LT : Nat -> Nat -> Set
67+total LT : Nat -> Nat -> Type
6868LT left right = LTE (S left) right
6969
70−total GT : Nat -> Nat -> Set
70+total GT : Nat -> Nat -> Type
7171GT left right = LT right left
7272
7373total lte : Nat -> Nat -> Bool
@@ -135,10 +135,10 @@ instance Num Nat where
135135 else
136136 O
137137
138−record Multiplicative : Set where
138+record Multiplicative : Type where
139139 getMultiplicative : Nat -> Multiplicative
140140
141−record Additive : Set where
141+record Additive : Type where
142142 getAdditive : Nat -> Additive
143143
144144instance Semigroup Multiplicative where
lib/Prelude/Strings.idr+1−1
@@ -8,7 +8,7 @@ import Prelude.Either
88
99-- Some more complex string operations
1010
11−data StrM : String -> Set where
11+data StrM : String -> Type where
1212 StrNil : StrM ""
1313 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
1414
lib/Prelude/Vect.idr+1−1
@@ -9,7 +9,7 @@ import Prelude.Nat
99
1010infixr 7 ::
1111
12−data Vect : Set -> Nat -> Set where
12+data Vect : Type -> Nat -> Type where
1313 Nil : Vect a O
1414 (::) : a -> Vect a n -> Vect a (S n)
1515
lib/System/Concurrency/Process.idr+1−1
@@ -12,7 +12,7 @@ data ProcID msg = MkPID Ptr
1212-- Type safe message passing programs. Parameterised over the type of
1313-- message which can be send, and the return type.
1414
15−data Process : (msgType : Set) -> Set -> Set where
15+data Process : (msgType : Type) -> Type -> Type where
1616 lift : IO a -> Process msg a
1717
1818instance Functor (Process msg) where
src/Core/CoreParser.hs+1−1
@@ -28,7 +28,7 @@ idrisDef = haskellDef {
2828 reservedOpNames
2929 = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
3030 reservedNames
31− = ["let", "in", "data", "codata", "record", "Set",
31+ = ["let", "in", "data", "codata", "record", "Type",
3232 "do", "dsl", "import", "impossible",
3333 "case", "of", "total", "partial", "mutual",
3434 "infix", "infixl", "infixr",
src/Idris/Parser.hs+1−1
@@ -760,7 +760,7 @@ pSimpleExpr syn =
760760 <|> try (do c <- pConstant
761761 fc <- pfc
762762 return (modifyConst syn fc (PConstant c)))
763− <|> do reserved "Set"; return PSet
763+ <|> do reserved "Type"; return PSet
764764 <|> try (do symbol "()"
765765 fc <- pfc
766766 return (PTrue fc))
test/reg001/reg001.idr+3−3
@@ -1,11 +1,11 @@
11apply : (a -> b) -> a -> b
22apply f x = f x
33
4−class Functor f => VerifiedFunctor (f : Set -> Set) where
4+class Functor f => VerifiedFunctor (f : Type -> Type) where
55 identity : (fa : f a) -> fmap id fa = fa
66
7−data Imp : Set where
8− MkImp : {any : Set} -> any -> Imp
7+data Imp : Type where
8+ MkImp : {any : Type} -> any -> Imp
99
1010testVal : Imp
1111testVal = MkImp (apply id O)
test/reg003/reg003.idr+2−2
@@ -1,12 +1,12 @@
11
22mutual
33 namespace Even
4− data EvenList : Set where
4+ data EvenList : Type where
55 Nil : EvenList
66 (::) : Nat -> OddList -> EvenList
77
88 namespace Odd
9− data OddList : Set where
9+ data OddList : Type where
1010 (::) : Nat -> EvenList -> OddList
1111
1212test : EvenList
test/reg003/reg003a.idr+2−2
@@ -1,9 +1,9 @@
11
2−data EvenList : Set where
2+data EvenList : Type where
33 ENil : EvenList
44 ECons : Nat -> OddList -> EvenList
55
6−data OddList : Set where
6+data OddList : Type where
77 OCons : Nat -> EvenList -> OddList
88
99test : EvenList
test/reg005/reg005.idr+1−1
@@ -4,7 +4,7 @@ rep : (n : Nat) -> Char -> Vect Char n
44rep O x = []
55rep (S k) x = x :: rep k x
66
7−data RLE : Vect Char n -> Set where
7+data RLE : Vect Char n -> Type where
88 REnd : RLE []
99 RChar : {xs : Vect Char k} ->
1010 (n : Nat) -> (x : Char) -> RLE xs ->
test/test001/test001.idr+4−4
@@ -2,18 +2,18 @@ module Main
22
33data Ty = TyInt | TyBool| TyFun Ty Ty
44
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
66interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n)
1111
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> Type where
1313 Nil : Env Nil
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
1717 stop : HasType fO (t :: G) t
1818 pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
@@ -22,7 +22,7 @@ using (G : Vect Ty n)
2222 lookup (pop k) (x :: xs) = lookup k xs
2323 lookup stop [] impossible
2424
25− data Expr : Vect Ty n -> Ty -> Set where
25+ data Expr : Vect Ty n -> Ty -> Type where
2626 Var : HasType i G t -> Expr G t
2727 Val : (x : Int) -> Expr G TyInt
2828 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
test/test002/test002.idr+5−5
@@ -1,7 +1,7 @@
11myid : a -> a
22myid x = x
33
4−idid : (a : Set) -> a -> a
4+idid : (a : Type) -> a -> a
55idid = myid ![myid]
66
77app : (a -> b) -> a -> b
@@ -15,14 +15,14 @@ doapp x = app myid x
1515
1616{-
1717
18−id : (b : Set k) -> b -> b : Set l, k < l
18+id : (b : Type k) -> b -> b : Type l, k < l
1919
20−foo = id ((a : Set k) -> a -> a) id
21− Set m, k < m
20+foo = id ((a : Type k) -> a -> a) id
21+ Type m, k < m
2222
2323So we have k < m, k < l, m <= k
2424
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
2626 if we can reach m from n, we have an inconsistency
2727
2828
test/test006/test006.idr+1−1
@@ -1,6 +1,6 @@
11module Main
22
3−data Parity : Nat -> Set where
3+data Parity : Nat -> Type where
44 even : Parity (n + n)
55 odd : Parity (S (n + n))
66
test/test007/test007.idr+1−1
@@ -4,7 +4,7 @@ data Expr = Var String
44 | Val Int
55 | Add Expr Expr
66
7−data Eval : Set -> Set where
7+data Eval : Type -> Type where
88 MkEval : (List (String, Int) -> Maybe a) -> Eval a
99
1010fetch : String -> Eval Int
test/test011/test011.idr+2−2
@@ -1,12 +1,12 @@
11module Main
22
3−record Foo : Nat -> Set where
3+record Foo : Nat -> Type where
44 MkFoo : (name : String) ->
55 (things : Vect a n) ->
66 (more_things : Vect b m) ->
77 Foo n
88
9−record Person : Set where
9+record Person : Type where
1010 MkPerson : (name : String) -> (age : Int) -> Person
1111
1212testFoo : Foo 3
test/test014/Resimp.idr+13−13
@@ -1,7 +1,7 @@
11module Resimp
22
33-- IO operations which read a resource
4−data Reader : Set -> Set where
4+data Reader : Type -> Type where
55 MkReader : IO a -> Reader a
66
77getReader : Reader a -> IO a
@@ -11,7 +11,7 @@ ior : IO a -> Reader a
1111ior = MkReader
1212
1313-- IO operations which update a resource
14−data Updater : Set -> Set where
14+data Updater : Type -> Type where
1515 MkUpdater : IO a -> Updater a
1616
1717getUpdater : Updater a -> IO a
@@ -21,7 +21,7 @@ iou : IO a -> Updater a
2121iou = MkUpdater
2222
2323-- IO operations which create a resource
24−data Creator : Set -> Set where
24+data Creator : Type -> Type where
2525 MkCreator : IO a -> Creator a
2626
2727getCreator : Creator a -> IO a
@@ -34,22 +34,22 @@ infixr 5 :->
3434
3535using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)
3636
37− data Ty = R Set
38− | Val Set
39− | Choice Set Set
40− | (:->) Set Ty
37+ data Ty = R Type
38+ | Val Type
39+ | Choice Type Type
40+ | (:->) Type Ty
4141
42− interpTy : Ty -> Set
42+ interpTy : Ty -> Type
4343 interpTy (R t) = IO t
4444 interpTy (Val t) = t
4545 interpTy (Choice x y) = Either x y
4646 interpTy (a :-> b) = a -> interpTy b
4747
48− data HasType : Vect Ty n -> Fin n -> Ty -> Set where
48+ data HasType : Vect Ty n -> Fin n -> Ty -> Type where
4949 stop : HasType (a :: gam) fO a
5050 pop : HasType gam i b -> HasType (a :: gam) (fS i) b
5151
52− data Env : Vect Ty n -> Set where
52+ data Env : Vect Ty n -> Type where
5353 Nil : Env Nil
5454 (::) : interpTy a -> Env gam -> Env (a :: gam)
5555
@@ -72,16 +72,16 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)
7272 envTail : Env (a :: gam) -> Env gam
7373 envTail (x :: xs) = xs
7474
75− data Args : Vect Ty n -> List Set -> Set where
75+ data Args : Vect Ty n -> List Type -> Type where
7676 ANil : Args gam []
7777 ACons : HasType gam i a ->
7878 Args gam as -> Args gam (interpTy a :: as)
7979
80− funTy : List Set -> Ty -> Ty
80+ funTy : List Type -> Ty -> Ty
8181 funTy list.Nil t = t
8282 funTy (a :: as) t = a :-> funTy as t
8383
84− data Res : Vect Ty n -> Vect Ty n -> Ty -> Set where
84+ data Res : Vect Ty n -> Vect Ty n -> Ty -> Type where
8585
8686{-- Resource creation and usage. 'Let' creates a resource - the type
8787 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
88pstring Reading = "r"
99pstring Writing = "w"
1010
11−data FILE : Purpose -> Set where
11+data FILE : Purpose -> Type where
1212 OpenH : File -> FILE p
1313
1414syntax ifM [test] then [t] else [e]
test/test015/Parity.idr+1−1
@@ -1,6 +1,6 @@
11module Parity
22
3−data Parity : Nat -> Set where
3+data Parity : Nat -> Type where
44 even : Parity (n + n)
55 odd : Parity (S (n + n))
66
test/test015/test015.idr+2−2
@@ -3,7 +3,7 @@ module Main
33import Parity
44import System
55
6−data Bit : Nat -> Set where
6+data Bit : Nat -> Type where
77 b0 : Bit O
88 b1 : Bit (S O)
99
@@ -15,7 +15,7 @@ instance Show (Bit n) where
1515
1616infixl 5 #
1717
18−data Binary : (width : Nat) -> (value : Nat) -> Set where
18+data Binary : (width : Nat) -> (value : Nat) -> Type where
1919 zero : Binary O O
2020 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
2121
test/test017/test017.idr+2−2
@@ -4,13 +4,13 @@ module scg
44
55data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
66
7−natElim : (n : Nat) -> (P : Nat -> Set) ->
7+natElim : (n : Nat) -> (P : Nat -> Type) ->
88 (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
99natElim O P mO mS = mO
1010natElim (S k) P mO mS = mS k (natElim k P mO mS)
1111
1212ordElim : (x : Ord) ->
13− (P : Ord -> Set) ->
13+ (P : Ord -> Type) ->
1414 (P Zero) ->
1515 ((x : Ord) -> P x -> P (Suc x)) ->
1616 ((f : Nat -> Ord) -> ((n : Nat) -> P (f n)) ->
tutorial/classes.tex+6−6
@@ -195,14 +195,14 @@ sortAndShow xs = show (sort xs)
195195\label{sec:monad}
196196
197197So 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,
199199and 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
201201declaration. For example:
202202
203203\begin{SaveVerbatim}{monad}
204204
205−class Monad (m : Set -> Set) where
205+class Monad (m : Type -> Type) where
206206 return : a -> m a
207207 (>>=) : m a -> (a -> m b) -> m b
208208
@@ -272,7 +272,7 @@ general, and applies to anything which is an instance of \texttt{MonadPlus}:
272272
273273\begin{SaveVerbatim}{monadplus}
274274
275−class Monad m => MonadPlus (m : Set -> Set) where
275+class Monad m => MonadPlus (m : Type -> Type) where
276276 mplus : m a -> m a -> m a
277277 mzero : m a
278278
@@ -363,7 +363,7 @@ class, which captures the notion of application for a data type:
363363
364364infixl 2 <$>
365365
366−class Applicative (f : Set -> Set) where
366+class Applicative (f : Type -> Type) where
367367 pure : a -> f a
368368 (<$>) : f (a -> b) -> f a -> f b
369369
@@ -420,7 +420,7 @@ Evaluation will take place relative to a context mapping variables (represented
420420
421421\begin{SaveVerbatim}{evalctxt}
422422
423−data Eval : Set -> Set where
423+data Eval : Type -> Type where
424424 MkEval : (List (String, Int) -> Maybe a) -> Eval a
425425
426426\end{SaveVerbatim}
tutorial/examples/binary.idr+2−2
@@ -1,6 +1,6 @@
11module Main
22
3−data Binary : Nat -> Set where
3+data Binary : Nat -> Type where
44 bEnd : Binary O
55 bO : Binary n -> Binary (n + n)
66 bI : Binary n -> Binary (S (n + n))
@@ -12,7 +12,7 @@ instance Show (Binary n) where
1212 show' (bI x) = show x ++ "1"
1313 show' bEnd = ""
1414
15−data Parity : Nat -> Set where
15+data Parity : Nat -> Type where
1616 even : Parity (n + n)
1717 odd : Parity (S (n + n))
1818
tutorial/examples/idiom.idr+1−1
@@ -4,7 +4,7 @@ data Expr = Var String
44 | Val Int
55 | Add Expr Expr
66
7−data Eval : Set -> Set where
7+data Eval : Type -> Type where
88 MkEval : (List (String, Int) -> Maybe a) -> Eval a
99
1010fetch : String -> Eval Int
tutorial/examples/interp.idr+4−4
@@ -2,18 +2,18 @@ module Main
22
33data Ty = TyInt | TyBool| TyFun Ty Ty
44
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
66interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n)
1111
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> Type where
1313 Nil : Env Nil
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
1717 stop : HasType fO (t :: G) t
1818 pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
@@ -21,7 +21,7 @@ using (G : Vect Ty n)
2121 lookup stop (x :: xs) = x
2222 lookup (pop k) (x :: xs) = lookup k xs
2323
24− data Expr : Vect Ty n -> Ty -> Set where
24+ data Expr : Vect Ty n -> Ty -> Type where
2525 Var : HasType i G t -> Expr G t
2626 Val : (x : Int) -> Expr G TyInt
2727 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
tutorial/examples/theorems.idr+1−1
@@ -8,7 +8,7 @@ twoPlusTwo = refl
88total disjoint : (n : Nat) -> O = S n -> _|_
99disjoint n p = replace {P = disjointTy} p ()
1010 where
11− disjointTy : Nat -> Set
11+ disjointTy : Nat -> Type
1212 disjointTy O = ()
1313 disjointTy (S k) = _|_
1414
tutorial/examples/universe.idr+2−2
@@ -1,7 +1,7 @@
1−myid : (a : Set) -> a -> a
1+myid : (a : Type) -> a -> a
22myid _ x = x
33
4−idid : (a : Set) -> a -> a
4+idid : (a : Type) -> a -> a
55idid = myid _ myid
66
77
tutorial/examples/views.idr+1−1
@@ -1,6 +1,6 @@
11module views
22
3−data Parity : Nat -> Set where
3+data Parity : Nat -> Type where
44 even : Parity (n + n)
55 odd : Parity (S (n + n))
66
tutorial/interp.tex+6−6
@@ -23,7 +23,7 @@ any other value:
2323
2424\begin{SaveVerbatim}{interpty}
2525
26−interpTy : Ty -> Set
26+interpTy : Ty -> Type
2727interpTy TyInt = Int
2828interpTy TyBool = Bool
2929interpTy (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
5151
5252\begin{SaveVerbatim}{exprdecl}
5353
54−data Expr : Vect Ty n -> Ty -> Set
54+data Expr : Vect Ty n -> Ty -> Type
5555
5656\end{SaveVerbatim}
5757\useverb{exprdecl}
@@ -63,11 +63,11 @@ constructor in turn.
6363
6464\begin{SaveVerbatim}{exprty}
6565
66−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
66+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
6767 stop : HasType fO (t :: G) t
6868 pop : HasType k G t -> HasType (fS k) (u :: G) t
6969
70−data Expr : Vect Ty n -> Ty -> Set where
70+data Expr : Vect Ty n -> Ty -> Type where
7171 Var : HasType i G t -> Expr G t
7272 Val : (x : Int) -> Expr G TyInt
7373 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,
8787
8888\begin{SaveVerbatim}{hastype}
8989
90−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
90+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
9191 stop : HasType fO (t :: G) t
9292 pop : HasType k G t -> HasType (fS k) (u :: G) t
9393
@@ -181,7 +181,7 @@ is defined in the context, we can then produce a value from the environment:
181181
182182\begin{SaveVerbatim}{envtype}
183183
184−data Env : Vect Ty n -> Set where
184+data Env : Vect Ty n -> Type where
185185 Nil : Env Nil
186186 (::) : interpTy a -> Env G -> Env (a :: G)
187187
tutorial/miscellany.tex+17−17
@@ -120,7 +120,7 @@ following function:
120120
121121\begin{SaveVerbatim}{interpfty}
122122
123−interpFTy : FTy -> Set
123+interpFTy : FTy -> Type
124124interpFTy FInt = Int
125125interpFTy FFloat = Float
126126interpFTy FChar = Char
@@ -137,7 +137,7 @@ can then be converted to an \Idris{} type:
137137
138138\begin{SaveVerbatim}{ffunty}
139139
140−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
140+ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
141141
142142\end{SaveVerbatim}
143143\useverb{ffunty}
@@ -149,10 +149,10 @@ A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
149149\begin{SaveVerbatim}{ftyex}
150150
151151Idris> ForeignTy [FInt, FString] FString
152−Int -> String -> IO String : Set
152+Int -> String -> IO String : Type
153153
154154Idris> ForeignTy [FInt, FString] FUnit
155−Int -> String -> IO () : Set
155+Int -> String -> IO () : Type
156156
157157\end{SaveVerbatim}
158158\useverb{ftyex}
@@ -164,7 +164,7 @@ converts this description to a function callable by \Idris{}
164164
165165\begin{SaveVerbatim}{mkForeign}
166166
167−data Foreign : Set -> Set where
167+data Foreign : Type -> Type where
168168 FFun : String -> (xs:List FTy) -> (t:FTy) ->
169169 Foreign (ForeignTy xs t)
170170
@@ -206,39 +206,39 @@ have types. For example:
206206\begin{SaveVerbatim}{typetypes}
207207
208208*universe> :t Nat
209−Nat : Set
209+Nat : Type
210210*universe> :t Vect
211−Vect : Set -> Nat -> Set
211+Vect : Type -> Nat -> Type
212212
213213\end{SaveVerbatim}
214214\useverb{typetypes}
215215
216216\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
218218
219219\begin{SaveVerbatim}{setset}
220220
221−*universe> :t Set
222−Set : Set
221+*universe> :t Type
222+Type : Type
223223
224224\end{SaveVerbatim}
225225\useverb{setset}
226226
227227\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
229229due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
230230of types (or \emph{universes}):
231231
232232\begin{SaveVerbatim}{sethierarchy}
233233
234−Set : Set 1 : Set 2 : Set 3 : ...
234+Type : Type 1 : Type 2 : Type 3 : ...
235235
236236\end{SaveVerbatim}
237237\useverb{sethierarchy}
238238
239239\noindent
240−Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that
241−\texttt{x : Set m}, as long as \texttt{n < m}.
240+Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that
241+\texttt{x : Type m}, as long as \texttt{n < m}.
242242The typechecker generates such universe
243243constraints and reports an error if any inconsistencies are found. Ordinarily, a
244244programmer does not need to worry about this, but it does prevent (contrived)
@@ -246,10 +246,10 @@ programs such as the following:
246246
247247\begin{SaveVerbatim}{idid}
248248
249−myid : (a : Set) -> a -> a
249+myid : (a : Type) -> a -> a
250250myid _ x = x
251251
252−idid : (a : Set) -> a -> a
252+idid : (a : Type) -> a -> a
253253idid = myid _ myid
254254
255255\end{SaveVerbatim}
@@ -257,7 +257,7 @@ idid = myid _ myid
257257
258258\noindent
259259The 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
261261than required if it is applied to itself.
262262
263263%\subsection{Comparison}
tutorial/modules.tex+1−1
@@ -208,7 +208,7 @@ constructors. They may also be dependent types with implicit arguments:
208208\begin{SaveVerbatim}{paramdata}
209209
210210parameters (xs : Vect a x, y : Nat)
211− data Vects : Set -> Set where
211+ data Vects : Type -> Type where
212212 MkVects : Vect a y -> Vects a
213213
214214 append : Vects a -> Vect a (x + y)
tutorial/provisional.tex+2−2
@@ -7,7 +7,7 @@ example, recall the \texttt{parity} function:
77
88\begin{SaveVerbatim}{pardecl}
99
10−data Parity : Nat -> Set where
10+data Parity : Nat -> Type where
1111 even : Parity (n + n)
1212 odd : Parity (S (n + n))
1313
@@ -230,7 +230,7 @@ case \texttt{Nat}):
230230
231231\begin{SaveVerbatim}{bindef}
232232
233−data Binary : Nat -> Set where
233+data Binary : Nat -> Type where
234234 bEnd : Binary O
235235 bO : Binary n -> Binary (n + n)
236236 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}:
7272
7373\begin{SaveVerbatim}{interval}
7474
75−data Interval : Set where
75+data Interval : Type where
7676 MkInterval : (lower : Float) -> (upper : Float) ->
7777 so (lower < upper) -> Interval
7878
tutorial/theorems.tex+2−2
@@ -8,7 +8,7 @@ the following definition:
88
99\begin{SaveVerbatim}{}
1010
11−data (=) : a -> b -> Set where
11+data (=) : a -> b -> Type where
1212 refl : x = x
1313
1414\end{SaveVerbatim}
@@ -45,7 +45,7 @@ to a successor:
4545disjoint : (n : Nat) -> O = S n -> _|_
4646disjoint n p = replace {P = disjointTy} p ()
4747 where
48− disjointTy : Nat -> Set
48+ disjointTy : Nat -> Type
4949 disjointTy O = ()
5050 disjointTy (S k) = _|_
5151
tutorial/typesfuns.tex+12−12
@@ -289,7 +289,7 @@ we declare vectors as follows:
289289
290290\begin{SaveVerbatim}{vect}
291291
292−data Vect : Set -> Nat -> Set where
292+data Vect : Type -> Nat -> Type where
293293 Nil : Vect a O
294294 (::) : a -> Vect a k -> Vect a (S k)
295295
@@ -305,7 +305,7 @@ Ambiguous constructor names can normally be resolved from context.
305305This declares a family of types, and so the form of the declaration is rather
306306different from the simple type declarations above. We explicitly state the type
307307of 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}
309309is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each
310310constructor targets a different part of the family of types. \tDC{Nil} can only
311311be used to construct vectors with zero length, and \tDC{::} to construct
@@ -370,7 +370,7 @@ They are declared as follows (again, in the prelude):
370370
371371\begin{SaveVerbatim}{findecl}
372372
373−data Fin : Nat -> Set where
373+data Fin : Nat -> Type where
374374 fO : Fin (S k)
375375 fS : Fin k -> Fin (S k)
376376
@@ -433,7 +433,7 @@ arguments to \texttt{index}. We could also write the type of \texttt{index} as:
433433
434434\begin{SaveVerbatim}{vindeximpty}
435435
436−index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
436+index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a
437437
438438\end{SaveVerbatim}
439439\useverb{vindeximpty}
@@ -481,7 +481,7 @@ definition, which defines a predicate on vectors:
481481
482482\begin{SaveVerbatim}{elem}
483483
484−data Elem : a -> Vect a n -> Set where
484+data Elem : a -> Vect a n -> Type where
485485 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)
486486 there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)
487487
@@ -513,7 +513,7 @@ ordering of any implicit arguments which can appear within the block:
513513\begin{SaveVerbatim}{elemusing}
514514
515515using (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
517517 here : Elem x (x :: xs)
518518 there : Elem x xs -> Elem x (y :: xs)
519519
@@ -674,7 +674,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:
674674
675675data List a = Nil | (::) a (List a)
676676
677−data Vect : Set -> Nat -> Set where
677+data Vect : Type -> Nat -> Type where
678678 Nil : Vect a O
679679 (::) : a -> Vect a k -> Vect a (S k)
680680
@@ -858,8 +858,8 @@ the value of the first element:
858858
859859\begin{SaveVerbatim}{sigma}
860860
861−data Exists : (A : Set) -> (P : A -> Set) -> Set where
862− Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P
861+data Exists : (A : Type) -> (P : A -> Type) -> Type where
862+ Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P
863863
864864\end{SaveVerbatim}
865865\useverb{sigma}
@@ -951,7 +951,7 @@ value is true:
951951
952952\begin{SaveVerbatim}{sotype}
953953
954−data so : Bool -> Set where
954+data so : Bool -> Type where
955955 oh : so True
956956
957957\end{SaveVerbatim}
@@ -1112,7 +1112,7 @@ can represent a person's name and age in a record:
11121112
11131113\begin{SaveVerbatim}{recsimpl}
11141114
1115−record Person : Set where
1115+record Person : Type where
11161116 MkPerson : (name : String) ->
11171117 (age : Int) -> Person
11181118
@@ -1165,7 +1165,7 @@ the record as a whole. For example:
11651165
11661166\begin{SaveVerbatim}{deprec}
11671167
1168−record Class : Set where
1168+record Class : Type where
11691169 ClassInfo : (students : Vect Person n) ->
11701170 (className : String) ->
11711171 Class
tutorial/views.tex+1−1
@@ -56,7 +56,7 @@ plus one:
5656
5757\begin{SaveVerbatim}{parity}
5858
59−data Parity : Nat -> Set where
59+data Parity : Nat -> Type where
6060 even : Parity (n + n)
6161 odd : Parity (S (n + n))
6262