idris-lang / idris-dev Goto Github PK
View Code? Open in Web Editor NEWA Dependently Typed Functional Programming Language
Home Page: http://idris-lang.org
License: Other
A Dependently Typed Functional Programming Language
Home Page: http://idris-lang.org
License: Other
If I try to :load
an absolute path from anywhere but the root directory, I get a "user error (Can't find import /path)".
An example session:
Idris> :load /Users/Tim/code/example.idr
user error (Can't find import /Users/Tim/code/example.idr)
I'm on OS X 10.6.8 with a Cabal-installed Idris 0.9.5.1 compiled with GHC 7.4.2 .
An analogue to GHCi's :info command would help with exploring typeclasses. I usually use this in GHCi just to see the class methods, but the enumeration of instances may be useful, too.
The following typechecks (and doesn't compile):
f : Nat -> Nat
f x = x + 1
foo : Nat -> Nat
foo (f x) = x
main : IO ()
main = putStrLn (show (foo 1))
Idris can't derive instances of data types automatically yet.
data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
deriving (Show, Eq, Ord, Bounded, Read)
The following code type checks
> module TestParameters > parameters (X : Set) > p : X -> Bool > p x = True > parameters (q : X -> Bool) > r : X -> Bool > r = q
But, replacing |q| by |p| in the last line yields
Can't unify (X : Set) -> X -> Bool with X -> Bool
This suggests that the parameter |X| is not passed to the nested |parameters| block and the type of |r| is not the same as the type of |p|. This is not how nested parameter blocks are supposed to be resolved.
I get this error when I try to execute the above:
INTERNAL ERROR: "{A0} is not a Set"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
I'm not sure if this is already covered by any of the other open issues.
data EvenList : Set where
ENil : EvenList
ECons : Nat -> OddList -> EvenList
data OddList : Set where
OCons : Nat -> EvenList -> OddList
test : EvenList
test = ECons 1 ENil --ENil is not an OddList
OddList is not defined yet, therefore EventList thinks OddList in the ECons Constructor is a typevariable.
I have found the proofs that I expect to be able to do in the form:
prf : ... -> a = b
prf ... with prf x'
| refl = refl
do not load properly giving an error "No such variable {x'0}". However in other cases matching on the I.H. with refl works just fine. A compete and fairly small example is pasted below. I hope this helps. I really like Idris. I want to start writing compilers in it.
module bug
data MNat = Z | S MNat
total add : MNat -> MNat -> MNat
add Z y = y
add (S x) y = S (add x y)
-- This proof checks just fine
total add0 : (x : MNat) -> (add x Z) = x
add0 Z = refl
add0 (S x') with (add0 x')
| ih = cong ih
-- However this one does not even load with an error: No such variable {x'0}
{-
total add0' : (x : MNat) -> (add x Z) = x
add0 Z = refl
add0 (S x') with (add0 x')
| refl = ?a
-}
total addxSy : (x : MNat) -> (y : MNat) -> (add x (S y)) = (S (add x y))
addxSy Z y = refl
addxSy (S x') y with (addxSy x' y)
| ih = cong ih
-- However this proof works just fine. And it also pattern matches over the ih with refl
total addSym : (x : MNat) -> (y : MNat) -> (add x y) = (add y x)
addSym Z y = sym (add0 y)
addSym (S x') y with (addSym x' y)
| refl = sym $ addxSy y y
Code:
test : String -> Int
test "yes" = 1
test "no" = 0
test str = -1
Result:
test.idr:9:warning - Unreachable case: test "no"
test.idr:9:warning - Unreachable case: test str
In fact, ∀x. test x = 1
. The same occurs when using a case-expression. Incidentally, pattern-matching does work for types other than String
.
Idris> :t _ _
(input):1:INTERNAL ERROR: "{a1} : Set 0 is not solved"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
(I think I copied that correctly)
You can get the same error by simply evaluating _ _ as well.
While trying to implement a Semigroup for Endomorphisms I found an interesting behavior.
data Endomorphism : Set -> Set where
Endo : (a -> a) -> Endomorphism a
test : Endomorphism Nat
test = f <+> f
where inc : Nat -> Nat
inc = (+1)
f : Endomorphism Nat
f = Endo inc
The following instance worked correctly:
instance Semigroup (Endomorphism a) where
f <+> g = Endo $ \a => g $ f $ a
*test *> test $ O
S (S O) : Nat
*test *> test $ 1
S (S (S O)) : Nat
Whenever using pattern matching the outcome is different:
instance Semigroup (Endomorphism a) where
(Endo f) <+> (Endo g) = Endo $ \a => g $ f a
*test> test $ 0
S O : Nat
*test> test $ 1
S (S O) : Nat
This is not quite what I expected. What's going on here?
I try to implement a length function for Vect like this
total annotateVector : Vect a n -> (n : Nat ** Vect a n)
annotateVector v = (_ ** v)
len : Vect a n -> Nat
len v = let (m ** v) = annotateVector v in m
The first function works fine, but when including the second function I get an error message saying:
No such variable {x1000}
The following code type checks
> module TestParameters
> -- parameters (
> X : Set --,
> Y : X -> Set --,
> step : (x : X) -> Y x -> X --,
> C : Set -> Set --,
> inC : X -> C X -> Bool --,
> someC : (X -> Bool) -> C X -> Bool --,
> lemmaC3 : (x : X) ->
> (p : X -> Bool) ->
> (xs : C X) ->
> so (p x) ->
> so (x `inC` xs) ->
> so (someC p xs) --,
> preds : X -> C X --,
> lemmaPreds1 : (x : X) ->
> (y : Y x) ->
> so (x `inC` (preds (step x y)))
> -- )
> reachable : (m : Nat) -> X -> Bool
> reachable O _ = True
> reachable (S m) x' = someC (reachable m) (preds x')
> reachableTh : (m : Nat) ->
> (x : X) ->
> so (reachable m x) ->
> (y : Y x) ->
> so (reachable (S m) (step x y))
> reachableTh m x rmx y = step3 where
> xs : C X
> xs = preds (step x y)
> step1 : so (x `inC` xs)
> step1 = lemmaPreds1 x y
> p : X -> Bool
> p = reachable m
> px : so (p x)
> px = rmx
> step2 : so (someC p xs)
> step2 = lemmaC3 x p xs px step1
> step3 : so (reachable (S m) (step x y))
> step3 = step2
However, uncommenting the parameter block yields
test_parameters_1.lidr:44:Can't unify Nat with Set
which seems to be inconsistent since the commented version does type check.
I'm not sure whether we really need such a function in Idris but anyway, I'll request it here for discussion.
In Haskell, there's a error
function, that's it's type signature:
error : String -> a
It causes run-time errors given the message to print. It can be sometimes useful.
We could implement this function with unsafePerformIO
or so which is also missing at the moment but which we could need in the future.
The following example:
module TestWhere
h : Bool -> Nat
h False = r1 where
r : Nat
r = S O
r1 : Nat
r1 = rh True = r2 where
r : Nat
r = O
r2 : Nat
r2 = r
yields the syntax "user error (test_where.lidr:13:r#TestWhere.h already defined)". I find this behavior disturbing: it is not consistent with Haskell (a corresponding Haskell version of the above example type checks without problems) and suggests scoping rules which I do not understand. It appears that the scope of the variable |r| defined in the first |where| clause goes beyond the first |where| block.
A consequence of this behavior is that the usage of |where| clauses in pattern matching becomes inpracticable as the number of patters increases. When pattern matching on a value of type |Vect 3 Bool|, for instance, all those |r111|, |r121|, |r212| etc. make programs difficult to read, maintain and extend and open the way to potentially dangerous errors.
seems like something where if possible, support should by default be doubles, or should both be supported?
I have run into this bug but much of this report is lifted from what Alan Pogrebinschi wrote in the email to the list: https://groups.google.com/forum/?fromgroups=#!topic/idris-lang/SsTCPqDKMko
[From Alan]
Idris> fmap id (Just 1) (input):0:Incomplete term fmap (id) (Just (fromInteger 1))
This effects some proofs. For instance,
[From Alan]
-- "Incomplete term" error class Functor f => VerifiedFunctor (f : Set -> Set) where identity : (fa : f a) -> fmap id fa = fa
However, it did work like this:
class Functor f => VerifiedFunctor (f : Set -> Set) where identity : (fa : f a) -> fmapid fa = fa -- Need this to avoid "Incomplete term" error fmapid : Functor f => f a -> f a fmapid = fmap id
The fact that this was not in the issue tracker seemed like an oversight. If that is not the case, sorry, and feel free to delete this. I'm still enjoying the time I spend with Idris.
For the datatypes
data IFin : Nat -> Set where
IfZ : {nat : Nat} -> IFin (S nat)
IfS : {nat : Nat} -> IFin nat -> IFin (S nat)
data EFin : Nat -> Set where
EfZ : (n : Nat) -> EFin (S n)
EfS : (n : Nat) -> EFin n -> EFin (S n)
ifinelim1
, ifinelim2
and ifinelim3
fail to typecheck but the explicit versions typecheck correctly:
-- Fully explicit
efinelim1 : (p : (n : Nat) -> EFin n -> Set) ->
((n : Nat) -> p (S n) (EfZ n)) ->
((n : Nat) -> (f : EFin n) -> p n f -> p (S n) (EfS n f)) ->
(n : Nat) -> (k : EFin n) -> p n k
efinelim1 p z s (S n) (EfZ _) = z n
efinelim1 p z s (S n) (EfS _ m) = s n m (efinelim1 p z s n m)
{- Can't unify IFin (S nat) with IFin (S n)
ifinelim1 : (p : (n : Nat) -> IFin n -> Set) ->
((n : Nat) -> p (S n) IfZ) ->
((n : Nat) -> (f : IFin n) -> p n f -> p (S n) (IfS f)) ->
(n : Nat) -> (k : IFin n) -> p n k
ifinelim1 p z s (S n) IfZ = z n
ifinelim1 p z s (S n) (IfS m) = s n m (ifinelim1 p z s n m)
-}
-- Implicit everything but z, s and the Fin
efinelim2 : {p : (n : Nat) -> EFin n -> Set} ->
((n : Nat) -> p (S n) (EfZ n)) ->
((n : Nat) -> (f : EFin n) -> p n f -> p (S n) (EfS n f)) ->
{n : Nat} -> (k : EFin n) -> p n k
efinelim2 z s (EfZ n) = z n
efinelim2 z s (EfS n m) = s n m (efinelim2 z s m)
{- Same error
ifinelim2 : {p : (n : Nat) -> IFin n -> Set} ->
((n : Nat) -> p (S n) IfZ) ->
((n : Nat) -> (f : IFin n) -> p n f -> p (S n) (IfS f)) ->
{n : Nat} -> (k : IFin n) -> p n k
ifinelim2 z s (IfZ {nat=n}) = z n
ifinelim2 z s (IfS {nat=n} m) = s n m (ifinelim2 z s m)
-}
-- Same but let Idris infer the Nats
efinelim3 : {p : (n : Nat) -> EFin n -> Set} ->
((n : Nat) -> p (S n) (EfZ n)) ->
((n : Nat) -> (f : EFin n) -> p n f -> p (S n) (EfS n f)) ->
{n : Nat} -> (k : EFin n) -> p n k
efinelim3 z s (EfZ _) = z _
efinelim3 z s (EfS _ m) = s _ m (efinelim3 z s m)
{- Same error
ifinelim3 : {p : (n : Nat) -> IFin n -> Set} ->
((n : Nat) -> p (S n) IfZ) ->
((n : Nat) -> (f : IFin n) -> p n f -> p (S n) (IfS f)) ->
{n : Nat} -> (k : IFin n) -> p n k
ifinelim3 z s IfZ = z _
ifinelim3 z s (IfS m) = s _ m (ifinelim3 z s m)
-}
If we explicitly pass n
to the constructors, it typechecks again:
ifinelime : (p : (n : Nat) -> IFin n -> Set) ->
((n : Nat) -> p (S n) (IfZ {nat = n})) ->
((n : Nat) -> (f : IFin n) -> p n f -> p (S n) (IfS {nat = n} f)) ->
(n : Nat) -> (k : IFin n) -> p n k
ifinelime p z s (S n) IfZ = z n
ifinelime p z s (S n) (IfS m) = s n m (ifinelime p z s n m)
In particular,
index (fS (fS (fS (fS fO)))) [1,2,3,4]
in the REPL causes the program to simply consume large amounts of memory and eventually die when killed by OOM. The REPL can be interrupted with ^C, at which point the memory used doesn't seem to be returned.
Bug observed in 0.9.2.1 on Arch Linux. Reproduced on master by Ralith.
The following program
> module TestParameters
> parameters (a : Nat)
> lala : Nat
|lala| is not defined
> parameters (b : Nat)
> lulu : Nat
does not type check:
"./test_parameters_2.lidr" (line 8, column 3):
unexpected "p"
expecting "public", "abstract", "private" or "class"
If one replaces the comment "|lala| is not defined" with "-- |lala| is not defined", however, it does !
The Haskell program
> module MA where
> type A = Bool
> module MB where
> import MA
> type B = A
> module TestExport where
> import MB
> i :: A -> B
> i = not
does not type check because, in |TestExport|, |A| is not visible. If one wants to use |MA.A| in |TestExport|, one has to import |MA|. This is good: if the names imported by a module were automatically injected in the namespaces of its clients, name clashes would hardly be avoidable. Maintaining and refactoring programs would be a nightmare: in order to find out the modules a program might depend upon, one would have to backwards reconstruct the whole import tree. In contrast, the Idris program
> module MA
> A : Set
> A = Bool
> module MB
> import MA
> B : Set
> B = A
> module TestExport
> import MB
> i : A -> B
> i = not
type checks. This suggests that the export rules of Idris might be fundamentally different from those of Haskell. Is this the case ? Why ?
its mentioned on the main site, and thats a relatively self contained bit, so I'd be interested in hacking on that
module Main
main : IO ()
main = putStrLn (show [1,2])
Idris version 0.9.5.1
The following code does not typecheck in both idris-0.9.2 and git
class Magma a where
comp : a -> a -> a
instance Magma Nat where
comp = plus
lemmaInc : (x : Nat) -> (y : Nat) -> (comp x (S y) = S (comp x y))
lemmaInc O n = refl
lemmaInc (S m) n with (lemmaInc m n)
| ind = ?lemmaInc_SA
thmComm : (x : Nat) -> (y : Nat) -> (comp x y = comp y x)
thmComm O O = refl
thmComm (S m) O with (thmComm m O)
| ind = ?thmComm_SO
thmComm m (S n) with (thmComm m n, lemmaInc m n)
| (ind, inc) = ?thmComm_AS
class (Magma a) => CommMagma a where
isComm : (x : a) -> (y : a) -> (comp x y = comp y x)
instance CommMagma Nat where
isComm = thmComm
---------- Proofs ----------
thmComm_SO = proof {
intros;
rewrite ind;
trivial;
}
thmComm_AS = proof {
intros;
rewrite ind;
rewrite inc;
trivial;
}
lemmaInc_SA = proof {
intros;
rewrite ind;
trivial;
}
Type checking ./test.idr
test.idr:25:Can't unify plus meth meth = plus meth meth with comp meth meth = comp meth meth
Specifically:
Can't unify plus with comp
Currently it's an ugly rendering with #s - maybe have them in a nested namespace, though careful not to make them accessible from the outer scope!
varad : Set -> Set -> Nat -> Set
varad Final Arg O = Final
varad Final Arg (S n) = Arg -> (varad Final Arg n)
varsum : {n : Nat} -> varad Nat Nat n
varsum {n=0} = 0
varsum {n=(S O)} x = x
varsum {n=(S (S m))} x y = varsum {n=(S m)} (x+y)
varsumo : {n : Nat} -> varad Int Int n
varsumo {n=O} = 0
varsumo {n=(S O)} = id
varsumo {n=(S (S m))} = (\x => (\y => varsumo {n=(S m)} (x+y)))
varsum and varsumo seem equivalent, but in the repl:
*varargs> varsumo {n=0}
0 : Int
*varargs> varsum {n=0}
varsum : Nat
*varargs> show $ varsumo {n=0}
"0" : String
*varargs> show $ varsum {n=0}
@prelude.Show$[Nat]#prelude.!show (varsum) : String
The following type checks
module bind
X : Set
R : X -> X -> Bool
f : (x0 : X) -> (x : X ** so (x0
R
x))test : (x : X) -> Bool
test k = True where
oops : (x' : X ** so (kR
x'))
oops = f k
However, replacing |k| with |x| in the definition of |test|, so that we have
test : (x : X) -> Bool
test x = True where
oops : (x' : X ** so (xR
x'))
oops = f x
raises a type error:
bind.lidr:12:Can't unify (x' ** so (R x x')) with (x ** so (R x x))
Which then goes away if we replace the name of the bound variable in the type of |f| by, say, |k|:
f : (x0 : X) -> (k : X ** so (x0
R
k))
The following example
> syntax [rel] [set] reflexive = (a : set) -> so (rel a a)
> Sub : (X : Set) -> (R1 : X -> X -> Bool) -> (R2 : X -> X -> Bool) -> Set
> Sub X R1 R2 = (x1 : X) -> (x2 : X) -> so (R1 x1 x2) -> so (R2 x1 x2)
type checks in a fraction of a second. This one
> syntax [rel] [set] reflexive = (a : set) -> so (rel a a)
> syntax [rel] [set] symmetric = {a : set} ->
> {b : set} ->
> so (rel a b) ->
> so (rel b a)
> Sub : (X : Set) -> (R1 : X -> X -> Bool) -> (R2 : X -> X -> Bool) -> Set
> Sub X R1 R2 = (x1 : X) -> (x2 : X) -> so (R1 x1 x2) -> so (R2 x1 x2)
takes about 10 seconds to type check. If one adds a third syntax extension
> syntax [rel] [set] reflexive = (a : set) -> so (rel a a)
> syntax [rel] [set] symmetric = {a : set} ->
> {b : set} ->
> so (rel a b) ->
> so (rel b a)
> syntax [rel] [set] transitive = {a : set} ->
> {b : set} ->
> {c : set} ->
> so (rel a b) ->
> so (rel b c) ->
> so (rel a c)
> Sub : (X : Set) -> (R1 : X -> X -> Bool) -> (R2 : X -> X -> Bool) -> Set
> Sub X R1 R2 = (x1 : X) -> (x2 : X) -> so (R1 x1 x2) -> so (R2 x1 x2)
type checking takes about 4 minutes. But if one comments out the last two lines, the syntax extensions alone type check in a second ! Importing such extensions in a code a bit longer than |Sub| leads to type checking times well beyond one hour !
Adding implicit arguments does not work correctly when named explicit arguments are given (which should report an error).
e.g.
foo : (a : Int) -> (b : Int) -> Int
foo {a=4} {b=3} should report an error.
Checking a swap function on Vectors fails with 'swap is not total as there are missing cases' even though the function is total
total
swap : {n : Nat} -> Vect A n -> Vect A n
swap Nil = Nil
swap (x :: Nil) = x :: Nil
swap (x :: y :: xs) = (y :: x :: (swap xs))
Same code checks fine in Agda
swap : {A : Set}{n : Nat} → Vec A n → Vec A n
swap [] = []
swap (x :: []) = x :: []
swap (x :: (y :: xs)) = y :: (x :: (swap xs))
Resolving dependencies...
Downloading idris-0.9.4...
Configuring idris-0.9.4...
Building idris-0.9.4...
Failed to install idris-0.9.4
Last 10 lines of the build log ( /Users/carter/.cabal/logs/idris-0.9.4.log ):
[1 of 1] Compiling Main (
/var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.4-23328/idris-0.9.4/Setup.hs,
/var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.4-23328/idris-0.9.4/dist/setup/Main.o
)
Linking
/var/folders/py/wgp_hj9d2rl3cx48yym_ynj00000gn/T/idris-0.9.4-23328/idris-0.9.4/dist/setup/setup
...
Configuring idris-0.9.4...
rm -f idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o libidris_rts.a
Building idris-0.9.4...
Preprocessing executable 'idris' for idris-0.9.4...
src/IRTS/Compiler.hs:9:8:
Could not find module `IRTS.CodegenJava'
Use -v to see a list of the files searched for.
cabal: Error: some packages failed to install:
idris-0.9.4 failed during the building phase. The exception was:
ExitFailure 1
not sure why i get this error
The appended code fails to type check with
test_injective.lidr:41:Can't verify injectivity of reachable m when unifying so (reachable m x) and so (p x)
I'm probably missing something but I do not see why |reachable m| is required to be injective (which in general is not) for |lemmaC3| to apply. The code type checks if line 41 is commented out and line 42 is uncommented.
module TestInjective
X : Set
Y : X -> Set
step : (x : X) -> Y x -> XC : Set -> Set
inC : X -> C X -> Bool
someC : (X -> Bool) -> C X -> Bool
lemmaC3 : (x : X) ->
(p : X -> Bool) ->
(xs : C X) ->
so (p x) ->
so (xinC
xs) ->
so (someC p xs)preds : X -> C X
lemmaPreds1 : (x : X) ->
(y : Y x) ->
so (xinC
(preds (step x y)))reachable : (m : Nat) -> X -> Bool
reachable O _ = True
reachable (S m) x' = someC (reachable m) (preds x')reachableTh : (m : Nat) ->
(x : X) ->
so (reachable m x) ->
(y : Y x) ->
so (reachable (S m) (step x y))
reachableTh m x rmx y = step3 where
xs : C X
xs = preds (step x y)
step1 : so (xinC
xs)
step1 = lemmaPreds1 x y
p : X -> Bool
p = reachable m
px : so (p x)
px = rmx
step2 : so (someC p xs)
step2 = lemmaC3 x p xs px step1
-- step2 = ?reachableTh_step2
step3 : so (reachable (S m) (step x y))
step3 = step2
I'm trying to prove the following lemma with the development version of
Idris:
total powerMultMultPower : (m : Nat) -> (n : Nat) -> (exp : Nat) ->
power m exp * power n exp = power (m * n) exp
powerMultMultPower m n O = refl
powerMultMultPower m n (S exp) =
let inductiveHypothesis = powerMultMultPower m n exp in
?powerMultMultPowerStepCase
In the proof of the step case, after performing "intros" and "compute",
I have the following proof state:
---------- Assumptions: ----------
m : Nat
n : Nat
exp : Nat
inductiveHypothesis : power m exp * (power n exp) = power (m * n) exp
---------- Goal: ----------
{ hole 4 }:
mult (mult m (power m exp)) (mult n (power n exp)) =
mult (mult m n) (power (mult m n) exp)
Applying "rewrite (multAssociative m (power m exp) (mult n (power n
exp)))" I get the following type error:
Can't unify Float -> Float with Nat.
It appears that the rewrite tactic is missing the fact that there is a
fixed variable of type Nat in the context with the name "exp" and is
instead trying to use the function "exp" of type Float -> Float (from
the Prelude?).
Also, if you mistakenly do:
"rewrite multAssociative" instead of the above, you get a message
warning about a missing error:
user error (INTERNAL ERROR: "Not an equality type"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues)
Presumably this should just warn about multAssociative not being applied
to enough arguments, rather than producing an internal error.
I'm trying to do a simple test for an interpreter that only knows constants and addition
module idr
data Expr : Set -> Set where
Const : Nat -> Expr Nat
Add : Expr Nat -> Expr Nat -> Expr Nat
eval : Expr a -> a
eval (Const a) = a
eval (Add a b) = eval a + (eval b)
mytest : {a, b : Nat} -> (eval (Add (Const a) (Const b))) = a + b
Interactive proving works fine…
Type checking ./test.idr
*test> :m
Global metavariables:
[idr.mytest]
*test> :p idr.mytest
---------- Goal: ----------
{ hole 0 }:
(a : Nat) ->
(b : Nat) ->
eval (Add (Const a) (Const b)) = a + b
-idr.mytest> intros
---------- Other goals: ----------
{ hole 1 }
{ hole 0 }
---------- Assumptions: ----------
a : Nat
b : Nat
---------- Goal: ----------
{ hole 2 }:
plus a b = plus a b
-idr.mytest> trivial
mytest: No more goals.
-idr.mytest> qed
idr.mytest = proof {
intros;
trivial;
}
*test> :addproof
Added proof idr.mytest
… and a proper proof section is added.
---------- Proofs ----------
idr.mytest = proof {
intros;
trivial;
}
However, loading the file results in an internal error:
raichoo@lain tmp» idris test.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.3
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./test.idr
test.idr:15:INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
*test>
Doing the proof manually works flawless.
mytest : {a, b : Nat} -> (eval (Add (Const a) (Const b))) = a + b
mytest = refl
src/Idris/Error.hs:34:14:
No instance for (MonadException (StateT IState (InputT IO)))
arising from a use of catch' Possible fix: add an instance declaration for (MonadException (StateT IState (InputT IO))) In the expression: catch In an equation for
idrisCatch': idrisCatch = catch
how do I fix that?
thanks :)
Idris> show $ zip [1,0] [1,9,3] refl
"[(1, 1), (9, 9), (3, 3)]" : String
Also of interest is that the first element of the second tuple is not 0.
This is on the latest git version.
When compiling I got as far as type-checking lib/Prelude/Complex.idr then got the error "hGetContents: invalid argument (invalid byte sequence)".
This happened with "cabal install idris" (version 0.9.5.1) and with a clone of commit cea7205
I changed the copyright header in that file from using a non-ASCII character to "(c)" and this made the error go away, allowing me to compile successfully. I don't know enough about Unicode handling in Haskell/Idris to stop this reoccuring, but I thought I'd raise the issue and my quick hack.
I'm running Debian unstable on an OLPC XO-1 laptop. Here are some possibly relevant numbers:
$ uname -a
Linux olpc 2.6.32-5-486 #1 Fri Dec 10 15:32:53 UTC 2010 i586 GNU/Linux
$ dpkg -l ghc | grep "ii"
ii ghc 7.4.1-4 i386 The Glasgow Haskell Compilation system
ii libghc-ansi-terminal-de 0.5.5-3+b1 i386 Simple ANSI terminal support, with Windows compatibi
ii libghc-ansi-wl-pprint-d 0.6.4-1+b1 i386 Wadler/Leijen Pretty Printer for colored ANSI termin
ii libghc-dlist-dev 0.5-3+b1 i386 Haskell library for Differences lists
ii libghc-hostname-dev 1.0-4+b1 i386 providing a cross-platform means of determining the
ii libghc-mtl-dev 2.1.1-1 i386 Haskell monad transformer library for GHC
ii libghc-quickcheck2-dev 2.4.2-1+b1 i386 Haskell automatic testing library for GHC
ii libghc-random-dev 1.0.1.1-1+b1 i386 Random number generator for Haskell
ii libghc-regex-base-dev 0.93.2-2+b2 i386 GHC library providing an API for regular expressions
ii libghc-regex-posix-dev 0.95.1-2+b1 i386 GHC library of the POSIX regex backend for regex-bas
ii libghc-smallcheck-dev 0.6-1+b1 i386 Another lightweight testing library
ii libghc-syb-dev 0.3.6.1-1 i386 Generic programming library for Haskell
ii libghc-test-framework-d 0.6-1+b1 i386 Framework for running and organising tests
ii libghc-test-framework-q 0.2.12.1-1+b1 i386 QuickCheck2 support for the test-framework package.
ii libghc-text-dev 0.11.2.0-1 i386 efficient packed Unicode text type for Haskell - GHC
ii libghc-transformers-dev 0.3.0.0-1 i386 Haskell monad transformer library
ii libghc-utf8-string-dev 0.3.7-1+b1 i386 GHC libraries for the Haskell UTF-8 library
ii libghc-x11-dev 1.5.0.1-1+b2 i386 Haskell X11 binding for GHC
ii libghc-xml-dev 1.3.12-1+b2 i386 A simple Haskell XML library - GHC libraries
ii libghc-xmonad-dev 0.10-4+b2 i386 Lightweight X11 window manager; libraries
$ ghc -v
Glasgow Haskell Compiler, Version 7.4.1, stage 2 booted by GHC version 7.4.1
Using binary package database: /usr/lib/ghc/package.conf.d/package.cache
Using binary package database: /home/chris/.ghc/i386-linux-7.4.1/package.conf.d/package.cache
hiding package text-0.11.2.0 to avoid conflict with later version text-0.11.2.3
hiding package mtl-2.1.1 to avoid conflict with later version mtl-2.1.2
wired-in package ghc-prim mapped to ghc-prim-0.2.0.0-bd29cb1ca1b712d64e00ac9207f87d0a
wired-in package integer-gmp mapped to integer-gmp-0.4.0.0-ec87c5d9609a1d46da031ef5d51c4f79
wired-in package base mapped to base-4.5.0.0-c8e7184681d410015e93df85fc49e9dd
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.7.0.0-fea440f2bc02cf9a412f25b6b74c4a70
wired-in package dph-seq not found.
wired-in package dph-par not found.
Hsc static flags: -static
*** Deleting temp files:
Deleting:
*** Deleting temp dirs:
Deleting:
ghc: no input files
Usage: For basic information, try the `--help' option.
$ file lib/Prelude/Complex.idr
lib/Prelude/Complex.idr: UTF-8 Unicode text
$ hexdump -C lib/Prelude/Complex.idr | head
00000000 7b 2d 0a 20 20 c2 a9 20 32 30 31 32 20 43 6f 70 |{-. .. 2012 Cop|
00000010 79 72 69 67 68 74 20 4d 65 6b 65 6f 72 20 4d 65 |yright Mekeor Me|
00000020 6c 69 72 65 0a 2d 7d 0a 0a 0a 6d 6f 64 75 6c 65 |lire.-}...module|
00000030 20 50 72 65 6c 75 64 65 2e 43 6f 6d 70 6c 65 78 | Prelude.Complex|
00000040 0a 0a 69 6d 70 6f 72 74 20 42 75 69 6c 74 69 6e |..import Builtin|
00000050 73 0a 69 6d 70 6f 72 74 20 50 72 65 6c 75 64 65 |s.import Prelude|
00000060 0a 0a 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d |..--------------|
00000070 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d |----------------|
00000080 20 52 65 63 74 61 6e 67 75 6c 61 72 20 66 6f 72 | Rectangular for|
00000090 6d 20 0a 0a 69 6e 66 69 78 20 36 20 3a 2b 0a 64 |m ..infix 6 :+.d|
If I type, e.g. in the REPL, fO {k = 996}, the output contains some strange items:
... (S (boolElim (Builtins.!>#@Builtins.Ord$[Int] 1 0 (boolElim (intToBool (prim__eqInt 1 0)) EQ (boolElim (intToBool (prim__ltInt 1 0)) Builtins.LT Builtins.GT))) (S O) O) ...
Until 995 it is fine :)
Thank you, and kind regards. Zenon
The following code
> module TestDeclDef > X : Set > X = (n : Nat ** so (n < 3)) > (==) : X -> X -> Bool > (==) x x' = (getWitness x == getWitness x') > data Move = L | R > adm : X -> Move -> Bool > adm (n ** _) L = n <= 1 > adm (n ** _) R = n >= 1 > step : (x : X) -> (m : Move) -> so (adm x m) -> X > step (O ** _) L _ = (2 ** oh) > step ((S n) ** _) L _ = (n ** believe_me oh) -- trivial > step (n ** _) R _ = > if n == 2 then (O ** oh) else (S n ** believe_me oh) > pred : X -> X -> Bool > pred x x' = (adm x L && x' == step x L (believe_me oh)) || > (adm x R && x' == step x R (believe_me oh)) > succs : X -> (n : Nat ** Vect X n) > succs x = filter (pred x) [(0 ** oh),(1 ** oh),(2 ** oh)] > succsTh : (x : X) -> so (not (getWitness (succs x) == O)) > succsTh x = ?lala
does not type check. One gets a
test_decl_def.lidr:29:Can't unify so True with so (adm x L)
at the last line, where |succsTh| is defined (well, almost). But if one moves the definition of |succs| from line 26 to somewhere after the definition of |succsTh|, the code type checks fine and the functions |pred| and |succs| can be called from the command line and behave as expected !
Thus it appears that deferring definitions sometimes helps type checking but ...
Currently, type signatures are not allowed in the interpreter. Instead, they lead to an error like in this example:
Idris> let list = ["foo","bar"] : List String in list
"(input)" (line 1, column 12):
unexpected reserved operator ":"
expecting "[", "if", "![", "?", "refl", "proof", "tactics", "case", operator, "(|", "[|", ")", ",", "**", identifier, "instance", "Integer", "Int", "Char", "Float", "String", "Ptr", float, natural, literal string, character, "Set", "()", "_|_", "_", "record", "\\", "let", "(", "|", "{" or "do"
This e.g. makes it impossible to define a list in a let-in-expression because the interpreter can't distinguish it from a vector.
In the following code, the definition of S_inj
is rejected by the current hackage version of Idris (0.9.2.1), which says there are missing cases but doesn't explain what they are. Even if this isn't a pattern coverage checking error, it would be nice to know what patterns it wants me to add.
module conat
data CoNat
= Co Nat
| Infinity
total S : CoNat -> CoNat
S (Co n) = Co (S n)
S Infinity = Infinity
total Sn_notzero : conat.S n = Co 0 -> _|_
total S_Co_not_Inf : S (Co n) = Infinity -> _|_
total S_inj : (n : CoNat) -> (m : CoNat) -> S n = S m -> n = m
S_inj (Co n) (Co m) refl = refl
S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)
S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))
S_inj Infinity Infinity refl = refl
The error reported is:
Type checking ./conat.idr
conat.idr:15:conat.S_inj is not total as there are missing cases
From a clumsier version of varsum:
varad : Set -> Set -> Nat -> Set
varad Final Arg O = Final
varad Final Arg (S n) = Arg -> (varad Final Arg n)
varsuma : {n : Nat} -> varad Nat Nat n
varsuma {n=(S O)} x = x
varsuma {n=(S (S m))} x = (\y => varsuma {n=(S m)} (x+y))
varsum : {n : Nat} -> varad Nat Nat n
varsum {n=0} = 0
varsum {n=m} = varsuma {n=m}
trying to use it:
*varargs2> varsum {n=0}
O : Nat
*varargs2> varsum {n=1} 1
O (S O) : Nat
so far so good
*varargs2> varsum {n=2} 1 2
O (S O) (S (S O)) : Nat
*varargs2> show $ varsum {n=2} 1 2
"O" : String
*varargs2> varsum {n=2} 5 7
O (S (S (S (S (S O))))) (S (S (S (S (S (S (S O))))))) : Nat
huh?
With HEAD as of this morning, I get the following error when trying to use a multi-arg lambda at the REPL:
*test> (\x, y => x + y) 3 2
(input):1:INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
*test> (\x, y => x `plus` y) 3 2
(input):1:INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
a : ((x : A) -> ()) -> ()
a x = ()
compiles, while
b : ({x : A} -> ()) -> ()
b x = ()
gives a parser error.
A comparable error occurs when constructing types on the right hand side of an =:
a : Set
a = (x : Int) -> ()
compiles, while
a : Set
a = {x : Int} -> ()
gives a parser error.
This interferes with construction of dependent function composition.
As far as I can tell. I could not install idris with "cabal install idris", until I had done "cabal install parsec". Output from cabal:
Downloading idris-0.9.5.1...
[1 of 1] Compiling Main ( /tmp/idris-0.9.5.1-9952/idris-0.9.5.1/Setup.hs, /tmp/idris-0.9.5.1-9952/idris-0.9.5.1/dist/setup/Main.o )
Linking /tmp/idris-0.9.5.1-9952/idris-0.9.5.1/dist/setup/setup ...
Configuring idris-0.9.5.1...
make: Entering directory /tmp/idris-0.9.5.1-9952/idris-0.9.5.1/rts' rm -f idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o libidris_rts.a make: Leaving directory
/tmp/idris-0.9.5.1-9952/idris-0.9.5.1/rts'
Building idris-0.9.5.1...
Preprocessing executable 'idris' for idris-0.9.5.1...
src/Idris/Parser.hs:25:18:
Could not find module `Text.Parsec.Token'
Idris' String type is just an array of (ascii-)chars, afaik. Unicode-support would be brilliant.
I thought |believe_me| could to be used as in the following example where, at line 8, |p x| is known to hold if |f| is evaluated but there is no way to prove it
> module TestBelieveMe > p : Nat -> Bool > f : (x : Nat) -> so (p x) -> Nat > r : Nat -> Nat -> Bool > r x x' = p x && x' == f x (believe_me oh) > nempty : (n : Nat ** Vect Nat n) -> Bool > succs : Nat -> (n : Nat ** Vect Nat n) > succs x = filter (r x) [0,1,2] > succsTh : (x : Nat) -> so (p x) -> so (nempty (succs x)) > succsTh x px = ?lala
This code, however, does not type check and I'm not sure that the error reported on the last line
test_believe_me.lidr:16:Can't unify so True with so (p x)
is correct (if one comments out line 16, the program type checks). Am I missing something obvious ?
The following code was hand-copied and might not be 100% accurate -- long story, I set up a new box, and I don't have X windows for it yet.
Here's the code:
module main
l : List Nat
l = [O]
l2 : List Int
l2 = [1]
total
rev : List a -> List a
rev l = reverse' l Nil
where
reverse' : List a -> List a -> List a
reverse' Nil acc = acc
reverse' (x :: xs) acc = reverse' xs (x :: acc)
main : IO ()
main = do
putStrLn (show l2)
putStrLn (show (rev l2))
Expected output was
[1]
[1]
Actual output is
[1]
[14557152]
It seems the usage of the variable l (line 11, column 18) is a reference to the global list l (line 3). It ought to be a reference to the function parameter l (line 11, column 5) instead.
The confusion bypasses the typechecker, and the result is garbage data, coerced into a string.
Place
the : (A : Set) -> A -> A
the _ = id
in a file and load it in the REPL, then execute:
Idris> the Int "foo"
"foo" : String
Strangely, values of type other than String seem to be correctly checked:
Idris> the Int [1,2,3]
Can't unify Vect a (S n) with Int
Idris> the String [1,2,3]
Can't unify Vect a (S n) with String
Idris> the String 42
(input):0:Can't convert Num Int with Num String
This bug does not appear to manifest with uses of 'the' in a file.
Currently, at least for me,
Idris> :t (->)
doesn't result in
Set -> Set -> Set
but instead prints this error:
"(input)" (line 1, column 1):
unexpected reserved operator "->", '>' or ':'
expecting "quit", "q", "help", "h", "?", "reload", "r", "edit", "e", "execute", "exec", "ttshell", "compile", "c", "metavars", "m", "prove", "p", "addproof", "a", "log", "spec", "hnf", "def", "d", "total", "[", "if", "![", "refl", "proof", "tactics", "case", "(|", "[|", identifier, "instance", "(", "Integer", "Int", "Char", "Float", "String", "Ptr", float, natural, literal string, character, "Set", "()", "_|_", "_", "record", "\\", "let", "|", "{", "do", "universes", "u", "dbginfo", "di", "info", "i", "search", "s", "x" or end of input
No such command
It'd be brilliant if this worked correctly.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.