idris - Relevance of model checking in strongly typed functional programming languages?

I am currently learning about model checking (modal logic, LTL, CTL, SAL model checker, etc.) and in my spare time I am learning about Idris which is a strongly typed functional programming language that supports dependent types. Since I am looking at both model checking and Idris, I start to get curious about how Idris relates to Formal Methods and model checking.When learning about model checking, it feels like most examples brought up is either about verifying systems written in an imperative manner or hardware components. So I am puzzled ab...Read more

idris - Lightyear requireFailure does not do backtracking

I want to parse a series of any 4 chars. However, these chars shouldn't form a specific string ( "bb" in an example below). So "aaaa" and "abcd" are okay, but neither "bbcd" nor "abbc" should not match.I composed a following parser:ntimes 4 (requireFailure (string "bb") *> anyChar)However, I noticed, that it "eats" single b chars. E.g.parse (ntimes 4 (requireFailure (string "bb") *> anyToken)) "abcde"results in ['a', 'c', 'd', 'e'] (it fails, however, on "bbcd" and "abbc" as expected).As a workaround I used my own implementation of requir...Read more

monoids - Idris - use same interface instance

I have a data structurerecord IdentityPreservingMorphism domain codomain whereconstructor MkMorphismOfMonoids func : domain -> codomain funcRespId : (Monoid domain, Monoid codomain) => func (Algebra.neutral) = Algebra.neutralwhich just says that an IdentityPreservingMorphism is a morphism between monoids which needs to respect the identity.I'm trying to prove that the identity morphisms is an IdentityPreservingMorphismmonoidIdentity : Monoid m => MorphismOfMonoids m mmonoidIdentity = MkMorphismOfMonoids id ?respIdThe easy shot for ...Read more

Slow type-checking and poor run-time performance with large natural numbers in Idris 1.2.0

I have been playing around with making my own random generator in Idris for learning purpose. In my solution I am aiming for totality for all functions and thus I am using numbers of type Nat and the built-in function modNatNZ which requires proof that the second arg isn't zero.While making a program to test my function on some large natural numbers as input, I encountered problems with both type checking and execution of the program being incredible slow.module Main%default totalgetUnixEpoch : IO IntgetUnixEpoch = foreign FFI_C "#(unsigned lon...Read more

idris - Left hand side of a generalized zip function never typechecks

I am trying to write a zip function in Idris that combines arbitrarily many vectors of the same length (len) into a single vector of HLists.That is, I am trying to generalize the following function:module Zipimport Data.Vect%default totalzip2 : (Vect len a, Vect len b) -> Vect len (a, b)zip2 ([], []) = []zip2 ((x :: xs), (y :: ys)) = (x, y) :: zip2 (xs, ys)I define my own HList ("heterogenous list") using vectors:data HList : Vect n Type -> Type where Nil : HList [] (::) : (x : a) -> (xs : HList as) -> HList (a :: as)Here is a va...Read more

typechecking - Idris Type mismatch that occurs even from template

Testing out an "easy" example of identity types, mod equality, but transitivity proof wont type check, even from the template. More than a fix, I want to know why?Here's a snippet of the minimal problemdata ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where {- 3 constructors reflexive: x == x (mod n), left-induct: x == y (mod n) => (x+n) == y (mod n) right-induct: x == y (mod n) => x == (y+n) (mod n) -} Reflex : (x:Nat) -> ModEq n x x --- Needs syntatic sugar, for now prefix LIn...Read more

idris - Working with types up to a certain equivalence

Suppose we'd like to represent (signed) integers as the Grothendieck group over naturals (or, in other words, as a pair (m, n), where the integer that's understood is m - n):data ZTy : Type where MkZ : (m, n : Nat) -> ZTyNow the (structural) equality that the language gives us for free is no longer what we want: instead, we only care about a certain equivalence relation (namely, (m1, n1) ~ (m2, n2) iff m1 + n2 = m2 + n1). No biggie, let's write this down!data Equiv : ZTy -> ZTy -> Type where MkEquiv : (prf : m1 + n2 = m2 + n1) ->...Read more

nix - How to resolve the issue "Can't find import Effects" in Idris?

I was trying to compile the following "hello world" source file after some time away from Idris using a nix-shell environment (direction):module Mainimport Effectsimport Effect.StdIOhello : Eff () [STDIO]hello = putStrLn "Hello world!"main : IO ()main = run helloMy output was as follows during the experimentation; despite specifying what seems to be the right library, I still get the same error at the end:[nix-shell:~/workspace/idris_tmp]$ idris --listlibs00prelude-idx.ibcprelude00base-idx.ibcbase[nix-shell:~/workspace/idris_tmp]$ exitexitbrand...Read more

reading and writing at Idris

I am in my first steps of learing "Idris". I am using this tutorial: created file called "hello.idr".The content of the file is :module Mainmain : IO ()main = putStrLn "Hello world"I enterd this line at the shell prompt:"idris hello.idr -o hello"but something unexcpeted occurred...Read more

idris - List of types from a function type

I would like to make a function that given a function type (e.g. String -> Nat -> Bool), would return a list of types corresponding to that function type (e.g. [String, Nat, Bool]). Presumably the signature of such a function would be Type -> List Type, but I am struggling to determine how it would be implemented....Read more

idris - Control.ST pure type

pure : (result : ty) -> STrans m ty (out_fn result) out_fn from'm not sure what (out_fn result) out_fn means. Is it about constraining out_fn to be a function of result? Does it actually say anything about the input resource list?The given explanation seems to be "...provided that the current list of resources is correct when producing that value" but I'm not sure how to interpret it....Read more

How can I use a proof I've made in Idris to inform the compiler that my type signature is correct?

I have a function count in idris, defined as :count : Eq a => a -> Vect n a -> Natcount x [] = Zcount x (y::ys) = with (x == y) | True = S (count x ys) | False = count x ysAnd a proof of the maximum value count can return:countLTELen : Eq a => (x : a) -> (l : Vect n a) -> LTE (count x l) ncountLTELen x [] = lteReflcountLteLen x (y::ys) with (x == y) | True = LTESucc (countLTELen x ys) | False = lteSuccRight (countLTELen x ys)which is all well and good. I now want to write a function which removes all of an element from a l...Read more

internals - Why does Idris think a prefix of an identifier is a keyword?

When trying to interpret this codeinjective : {A : Type} -> {P : A -> Type} -> ((x : A) -> P x) -> TypeI get the error |14 | injective : {A : Type} -> | ^not a terminatorwhich really confused my. When I write private over the declaration, the error seems to go away, so I guess those access modifiers really change the way parsing works. However, I don't understand why that should be.So why does that error show up? Why does the parser think in is a keyword (which I'm guessing is the...Read more

Idris: Implicit parameters in records

When I try to compile this examplerecord R where f: () -> {t: Type} -> tI get this error:Type mismatch between () -> t1 (Type of f)and () -> t (Expected type)Specifically: Type mismatch between t1 and tOn the other hand this examplerecord R where f: {t: Type} -> () -> tworks just fine. Can you tell me what's wrong with the first one?...Read more

Why do I need the Identity functor in Idris

Although Idris is dependently typed, where values can be used freely in types, it still differentiate function id and functor Identity. Why can't I define Functor instances on id:Functor id where map = idThe type of id is id : a -> a, why can't a be unified with Type, so that map @{Functor id} has type (a -> b) -> id a -> id b, which is just (a -> b) -> a -> bI understand that Identity is a type wrapper but why do I need a separate id at type level, just to enable the implementation of typeclass instances.The only differen...Read more