Comments (5)
There is a syntax error in line 9. Due to some issues in the parser, it's getting eaten and the failure is propagating up and giving the wrong parse error.
Here, Idris is expecting a term:
AppendSame : (val : Nat) -> Broadcastable (v1 : Vect n Nat) (v2 : Vect n Nat) -> Broadcastable (val :: v1) (val :: v2)
^^^^^^^^^^^^^^^^^
You can put v1
there. Idris automatically adds {0 v1 : _} ->
at the beginning. If you want to specify that v1
and v2
are the same length, you'll have to manually write out the implicits:
import Data.Vect
data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
Empty : Broadcastable [] []
AppendSame : {0 v1 : Vect n Nat} -> {0 v2 : Vect n Nat} -> (val : Nat) -> Broadcastable v1 v2 -> Broadcastable (val :: v1) (val :: v2)
Hopefully that unblocks you, but IMO we need a better parse error here.
from idris2.
I prefer the solution I gave above, by you could also do this:
data Broadcastable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
Empty : Broadcastable [] []
AppendSame : (val : Nat) -> Broadcastable (the (Vect n Nat) v1) (the (Vect n Nat) v2) -> Broadcastable (val :: v1) (val :: v2)
The the
function is identity with the type made explicit. It is used in Idris where an inline type annotation might be used in another language. If you do this, and type :ti AppendSame
in the repl, you'll see that Idris adds the two implicits that I wrote above, but in the opposite order.
from idris2.
Thanks! Broadcastable
is now working properly.
However, I have one other similar issue. For my other type:
data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
Dim2 : ([r1, c1]: Vect 2 Nat) -> ([c1, c2]: Vect 2 Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]
I get the error
Error: Expected a type declaration.
main:16:10--16:11
12 | AppendOneLeft : (right: Nat) -> (b: Broadcastable v1 v2) -> Broadcastable (1::v1) (right::v2)
13 | AppendOneRight : (left: Nat) -> (b: Broadcastable v1 v2) -> Broadcastable (left::v1) (1::v2)
14 |
15 | data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
16 | Dim2 : ([r1, c1]: Vect 2 Nat) -> ([c1, c2]: Vect 2 Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]
^
Error: Undefined name unsafePerformIO.
(Interactive):1:1--1:1
1 | module Main
How might this be resolved?
from idris2.
This is because pattern matching on the left side of :
is not supported.
This should work although it does not do what you're looking for wrt to line-column checking:
data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
Dim2 : (v1: Vect 2 Nat) -> (v2: Vect 2 Nat) -> MatrixMultiplicable v1 v2
The most naive way of checking that the size of two matrices match is to write multiplication directly with the following type:
Matrix : Nat -> Nat -> Type -> Type
Matrix a b ty = Vect a (Vect b ty)
multiply : Matrx a b ty -> Matrix b c ty -> Matrix a c ty
multiply = ?etc
from idris2.
I resolved the issue by parameterizing the matrix dimensions as follows
data MatrixMultiplicable : (Vect n1 Nat) -> (Vect n2 Nat) -> Type where
Dim2 : (r1: Nat) -> (c1: Nat) -> (c2: Nat) -> MatrixMultiplicable [r1, c1] [c1, c2]
from idris2.
Related Issues (20)
- [ perf ] type-level evalutaion of `Prelude.elem` is slow compared to the naïve implementation
- Loss of Linearity in Interaction of Abstract Interfaces and Linear State Transformer Monad HOT 5
- Is it safe to pass a GC'ed pointer to C?
- Underscore name of an implicit argument in a signature of an interface function does not work
- Chez backend is too naive on the value of `CHEZ` environment variable
- unification failure between if then else statements when using isYes (decEq n a) as the condition HOT 2
- Add error message with missing fixity namespace
- Execution and compilation hangs indefintely HOT 3
- Loading file in ide-mode changes working directory and causes errors on later actions
- Make output of ide-mode `:interpret` consistent to always return consistent datatype (String)
- Inconsistent error message when finding more than one implementation of an interface
- Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker HOT 8
- Support type annotations on LHS of a monadic bind `<-` HOT 9
- Incremental compilation includes some but not all metas
- Test idris2/reflection/reflection024 fails due to not accounting for locales
- Nested code blocks are ignored in literate markdown HOT 1
- Bootstrap with Racket error: `raco: Unrecognized command: exe` HOT 3
- Why quoted values are EmptyFC?
- Totality checker inconsistency when using Inf HOT 2
- Case split doesn't detect cases when working inside a namespace
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris2.