Idris' String type is just an array of (ascii-)chars, afaik. Unicode-support would be brilliant.

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|

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.

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.

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'

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 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.

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 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 ?

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))

module Main

main : IO ()
main = putStrLn (show [1,2])

Idris version 0.9.5.1

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 -> 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
-- step2 = ?reachableTh_step2
step3 : so (reachable (S m) (step x y))
step3 = step2

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.

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.

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 !

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

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?

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 foridrisCatch': idrisCatch = catch

how do I fix that?

thanks :)

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

seems like something where if possible, support should by default be doubles, or should both be supported?

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 ...

• Is this a feature or a bug ?
• Should the code type check no matter where |succs| is defined ? Why ?
• Should the type checker always reject the code ? Why ?
• Should the type checker behave as it does ? Why ?

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.

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 ?

its mentioned on the main site, and thats a relatively self contained bit, so I'd be interested in hacking on that

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.

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

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

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.

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.

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

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.

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.

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.

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))

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.

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 !

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 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}

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 = r

h 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.

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.

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 (k R 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 (x R 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))

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

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)

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

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?

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

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.

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 .