edwinb / idris2-boot Goto Github PK
View Code? Open in Web Editor NEWA dependently typed programming language, a successor to Idris
Home Page: https://idris-lang.org/
License: Other
idris2-boot's People
Contributors
Stargazers
Watchers
Forkers
vitalibarozzi ska80 chrrasmussen silky melted kristleifur paulyc alf239 abailly mmhelloworld petithug simonchatts pmwhite nightscape rmdouglas steshaw timsueberkrueb akuhlens luochen1990 thautwarm guenchi ohad msmorgan vikfret moranski andrevidela stjordanis joserfjuniorllms milankral spy joulroad matthew-hilty alrunner4 rbarreiro m-bd ziman acatton deviant-forks e-dt then0rth jeetu7 maxdeviant librecybernetics evertedsphere porges terkwood kftygy4aquzoi abdelq kaiepi cypheon mokshasoft berewt marcesquerra andylokandy tomkpz karroffel haoyuchen1014idris2-boot's Issues
Can't build Idris2 on Mac OS X
I am trying to build Idris2 on Mac OS X. I have previously installed ChezSchem, building with ./configure --threads && make && make install:
$ scheme
Chez Scheme Version 9.5.2
Copyright 1984-2019 Cisco Systems, Inc.
>
when I run make into a freshly checked out directory, I got the following errors in tests:
Found Chez Scheme at /usr/local/bin/scheme
Exception: variable make-thread-parameter is not bound
chez/chez001: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez002: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez003: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez004: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez005: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez006: FAILURE
Exception: variable make-thread-parameter is not bound
chez/chez007: FAILURE
119/126 tests successful
make[1]: *** [test] Error 1
make: *** [test] Error 2
Unexpected run-time complexity
The program
import Data.Fin
import Data.Vect
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = ...
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
main : IO ()
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
type checks and executes in more than quadratic time in N in idris 2:
N = 20, user time = 0.78s
N = 40, user time = 2.57s
N = 80, user time = 14.49s
N = 160, user time = segfault
N = 320, user time = segfault
For "large" values of N, it segfaults. In idris 1, the correspondent program also does not run in linear time
N = 100, user time = 3.3s
N = 200, user time = 4.9s
N = 400, user time = 10.1s
N = 800, user time = 36.4s
N = 1600, user time = 197.6s
, but it does not segfault and is faster. What is the expected complexity of the program? Shouldn't building the vector and reading its last component be linear operations in N?
Auto implicits aren't added to the scope
Steps to Reproduce
module Temp
import Data.List
safeHead : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead [] = absurd pr
safeHead (x::xs) = x
Expected Behavior
Compiles successfully.
Observed Behavior
Temp.idr:6:18--7:1:While processing right hand side of Temp.head at Temp.idr:6:1--7:1:
Undefined name pr
The snippet works when auto is removed or the implicit is introduced manually:
safeHead [] {pr} = absurd pr
Feature requests and proposals
If you have a feature request or proposal, or if you're looking for a place to get started contributing to Idris 2, please take a look at https://github.com/edwinb/Idris2/wiki/Contributions-wanted, or at https://github.com/edwinb/Idris2/blob/master/CONTRIBUTING.md
At the moment, since it's (mostly) only me working on the project, in about half my time, this is mainly in an effort to prevent the issue tracker for getting out of control, and making sure that I can keep on top of the most important bugs.
Please feel free to discuss proposals via the wiki or the mailing list, however!
Interpreter does not clean opened files when loading/reloading files
The interpreter blows up very quickly when one loads a file too many times, yielding a too many open files error that seems irrecoverable.
Steps to Reproduce
- Create some Idris source file
Source.idr, possibly valid or invalid it does not matter - Create an
inputfile containing about 50 lines like::l Source.idr - Run
Idris2 < input
Observed Behavior
Text.Parse> 2/2: Building Text.Parse (Text/Parse.idr)
(implicit):1:1--1:1:Builtin not found
PrimIO> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Main> File error in Text/Parse.idr: Too many open files
Expected Behavior
Files should be closed when reloaded and interpreter should not blow up unless one tries to load 100s or 1000s of files.
Implicit record fields
Steps to Reproduce
module Temp
import Data.Vect
record Foo where
constructor MkFoo
filler : Int
{size : Nat}
foos : Vect size String
isEmpty : Foo -> Bool
isEmpty f = size f == 0
Expected Behavior
This compiles and works as expected both with and without the filler field in Idris 1.3.
Observed Behavior
Without filler:
Temp.idr:8:3--8:3:Parse error: Expected end of input (next tokens: [identifier foos, symbol :, identifier Vect, identifier size, String, identifier isEmpty, symbol :, identifier Foo, symbol ->, identifier Bool])
With filler:
Temp.idr:12:13--12:20:While processing right hand side of Temp.isEmpty at Temp.idr:12:1--13:1:
Undefined name size
weird error when trying to build
When I make I get
Type checking ./Core/Core.idr
./Core/Core.idr:402:12:
|
402 | traverse : (a -> Core b) -> Binder a -> Core (Binder b)
| ^
When checking type of traverse:
Can't disambiguate name: Language.Reflection.Binder, Core.TT.Binder
make: *** [idris2] Error 1
This is strange because I can't see Language.Reflection.Binder anywhere in the Idris2 code base, why does it think Core.idr is importing it somehow?
Nat is not optimized correctly in all cases, leading to run-time error
When using Nat's successor (S) as a function, it is not optimized correctly, leading to run-time error.
If I disable the natHack and natHackTree in Compiler.CompileExpr module, the example below works as expected. I can also rewrite the expression S to (\n => S n) and it will now be optimized correctly.
I first discovered this issue when using the range syntax to create a List Nat. It was the functions rangeFromTo and rangeFrom from the Nat implementation of Range that lead me to the problem, more specifically the expression countFrom x S.
I am able to reproduce this issue using both the Chez and Racket code generators (I did not try Chicken).
Steps to Reproduce
Create a file called Nat.idr and execute it: idris2 --exec main Nat.idr
myS : Nat -> Nat
myS n = S n
myS_crash : Nat -> Nat
myS_crash = S
main : IO ()
main = do
printLn (S Z)
printLn (myS Z)
printLn (myS_crash Z)
Expected Behavior
Output:
1
1
1
Observed Behavior
Output:
1
1
Exception in number->string: #(1 0) is not a number
Build fails with "no such variable clockTime"
Full error is below. I searched for a definition of clockTime but didn't find anything. I'm building by running make idris2 in a freshly-cloned repo.
Type checking ./Core/Context.idr
./Core/Context.idr:1815:7-1830:20:
|
1815 | = do opts <- getSession
| ~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of logTime with expected type
Core a
When checking an application of function Core.Core.coreLift:
No such variable clockTime
make: *** [idris2] Error 1
New release of Idris1 to hackage to build Idris2
Could someone release the latest idris package to hackage. I want a more stable build environment for idris 2 using nix but really to do that I need the version of idris 1 required to be on Hackage so that I can update nixpkgs etc etc.
Error building Idris2: No such variable clockTime
I checked out this repo (commit 38443e2), ran make idris2, and got the following error. I'm using Version 1.3.1 of Idris1 to build.
(Note that I'm not very familiar with Idris so it's possible I'm doing something horribly wrong).
Type checking ./Core/Context.idr
./Core/Context.idr:1790:7-1805:20:
|
1790 | = do opts <- getSession
| ~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of logTime with expected type
Core a
When checking an application of function Core.Core.coreLift:
No such variable clockTime
make: *** [Makefile:10: idris2] Error 1
When I grep the repo for clockTime I see no other references outside of that file.
Option --no-prelude is not honoured when not loading a file
Starting idris2 without prelude and without loading a file fails:
$ ./idris2 --no-prelude
Uncaught error: Error in TTC file: TTC data is in an older format
Investigating this issue a little bit, I found this comes from the following fragment in Main.idr:
case fname of
Nothing => logTime "Loading prelude" $
readPrelude
Just f => logTime "Loading main file" $
loadMainFile f
Fix is pretty simple: Check noprelude option in session, I will submit a PR for this.
Elm style compiler error messages
If you've not seen Elm's compiler error messages they are simply awesome, check out https://elm-lang.org/blog/compiler-errors-for-humans
I think they very much fit in with the Idris philosophy of the compiler being your friend and guide rather than a gate keeper enemy. I was thinking, would the Idris compiler be capable of making suggestions based on the same mechanism used for type holes? For example if I have the following:
f : Int -> Int
f x = ?f_rhsand I check the type of ?f_rhs I get
Idris: Type of f_rhs
x : Int
-------------------------------------
f_rhs : Int
Now consider an example where I implement f incorrectly
f : Int -> Int
f x = yIt would be nice if the compiler error message was something like
`y` is undefined
you need something of type Int and have the following terms available
x : Int
perhaps you meant
f x = x
Is this possible in theory? I was thinking of taking a look but I haven't looked at the code base yet, it's going to take a long while to get my head around it I think. Does anyone have any pointers on where to begin looking for this feature specifically?
Mismatch
The program
import Data.List
import Data.List.Elem
interface Set t st where
Elem : t -> st -> Type
a1 : (x : t) -> DPair st (Elem x)
a2 : (x : t) -> (xs : st) -> Dec (Elem x xs)
Empty : st -> Type
Empty xs = (x : t) -> Not (Elem x xs)
fails to type check with
nicola@cirrus:~/gitlab/botta/Idris2Libs$ idris2 issues/Mismatch1.idr
1/1: Building issues.Mismatch1 (issues/Mismatch1.idr)
issues/Mismatch1.idr:11:37--11:39:While processing right hand side of Main.Default implementation of Empty at issues/Mismatch1.idr:11:3--12:1:
When unifying st and List t
Mismatch between:
st
and
List t
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main>
This seems an Idris bug: commenting out
import Data.List.Elem
makes the program type check perfectly.
Add option to compile to CLI
Steps to Reproduce
idris2 --compile myproject.ipkg
Expected Behavior
A chez scheme file is produced (unless you select a different --codegen)
Observed Behavior
--compile flag does not exist
The reason for this is that when building an executable that I want to distribute, I don't want to use the REPL or ide interface, especially in a CI system or if using a build and package manager like bazel or nix.
Implicits (and auto implicits) don't get passed to "with" clauses
Steps to Reproduce
module Temp
import Data.List
safeStrHead : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead s with (unpack s)
safeStrHead s | [] = absurd pr
safeStrHead s | (c::_) = c
Expected Behavior
Compiles successfully.
Observed Behavior
Temp.idr:7:31--8:3:While processing right hand side of Temp.with block in 1163 at Temp.idr:7:3--8:3:
Undefined name pr
Can be made to compile by changing to:
safeStrHead : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
safeStrHead {pr} s with (unpack s)
safeStrHead {pr} s | [] = absurd pr
safeStrHead s | (c::_) = c
When pr is made an auto implicit, both the version above and the one with @{pr} work (but not the initial one without manual introductions).
Interfaces and records: unexpected behavior
The program
module issues.FiniteAsRecord
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
record Iso a b where
constructor MkIso
to : a -> b
from : b -> a
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
record Finite t where
constructor MkFinite
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect (card t) t
foo = toVect (from iso)
type checks fine in Idris 2. But
module issues.FiniteAsInterface
import Data.Fin
import Data.Vect
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
record Iso a b where
constructor MkIso
to : a -> b
from : b -> a
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
interface Finite t where
card : Nat
iso : Iso t (Fin card)
foo : (Finite t) => Vect (card t) t
foo = toVect (from iso)
fails to type check with
nicola@cirrus:~/gitlab/botta/Idris2Libs$ idris2 issues/FiniteAsInterface.idr
1/1: Building issues.FiniteAsInterface (issues/FiniteAsInterface.idr)
issues/FiniteAsInterface.idr:24:27--24:33:While processing type of issues.FiniteAsInterface.foo at issues/FiniteAsInterface.idr:24:1--25:1:
When unifying Nat and Type -> Nat
Mismatch between:
Nat
and
Type -> Nat
issues/FiniteAsInterface.idr:25:1--26:1:No type declaration for issues.FiniteAsInterface.foo
Welcome to Idris 2 version 0.0. Enjoy yourself!
issues.FiniteAsInterface>
Is this the expected behavior?
In absence of a mechanism for referring to the cardinality of t in the signature of foo, one is forced to implement foo as a default method of the Finite interface. This leads to "fat" interfaces which is usually considered a bad design. Does this mean that, in order to keep interfaces "thin" we should use records instead of interfaces? What are the advantages/disadvantages of records vs. interfaces?
Cannot solve constraint: bug or expected behavior
The program
module issues.CannotSolveConstraint3
Surjective : {s, t : Type} -> (f : s -> t) -> Type
Surjective {s} {t} f = (y : t) -> DPair s (\ x => f x = y)
NonSurjective : {s, t : Type} -> (f : s -> t) -> Type
NonSurjective {s} {t} f = DPair t (\ y => (x : s) -> Not (f x = y))
nonSurjectiveNotSurjective : {s, t : Type} -> (f : s -> t) -> NonSurjective f -> Not (Surjective f)
nonSurjectiveNotSurjective f (MkDPair y faxnfxy) =
\ surjectivef => let x = fst (surjectivef y) in (faxnfxy x) (snd (surjectivef y))
type checks in Idris 1 but in not in Idris 2:
nicola@cirrus:~/gitlab/botta/Idris2Libs$ idris2 issues/CannotSolveConstraint3.idr
1/1: Building issues.CannotSolveConstraint3 (issues/CannotSolveConstraint3.idr)
issues/CannotSolveConstraint3.idr:11:64--11:83:While processing right hand side of issues.CannotSolveConstraint3.nonSurjectiveNotSurjective at issues/CannotSolveConstraint3.idr:10:1--13:1:
Can't solve constraint between:
fst (surjectivef y)
and
x
Welcome to Idris 2 version 0.0. Enjoy yourself!
issues.CannotSolveConstraint3>
Is this the expected behavior or an Idris 2 issue?
Can't solve constraint (interface method issue)
The program
module issues.CannotSolveConstraint2
import Data.Fin
import Data.Vect
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
record Iso a b where
constructor MkIso
from : b -> a
interface Finite t where
card : Nat
iso : Iso t (Fin card)
foo : Vect card t
foo = toVect (from iso)
type checks fine in Idris1 but not in Idris2.
The issue seems to be that, in Idris2, card in the signature of foois not taken to be the card method of the interface but an implicit argument.
Unable to solve constraint with Fin.fromInteger
Steps to Reproduce
module Main
import Data.Vect
data HVect : Vect n Type -> Type where
Nil : HVect []
(::) : t -> HVect ts -> HVect (t :: ts)
replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
replaceAt FZ y (x :: xs) = y :: xs
replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs
wat : Bool -> HVect [Bool] -> HVect [Bool]
wat x xs = replaceAt 0 x xsExpected Behavior
The function wat should type check, as it does with Idris 1.3.2.
Observed Behavior
wat.idr:22:12--24:1:While processing right hand side of Main.wat at wat.idr:22:
1--24:1:
Can't solve constraint between:
replaceAt fromInteger 0 Bool [Bool]
and
[Bool]
The program does compile successfully when the argument 0 is replaced with FZ. I find this error message to be misleading since it seems unclear to me what constraint the compiler is struggling with.
Infinite loop with hole
Hi there,
Just to let you know, there is an infinite loop (100% CPU utilization) when a hole reuse a name:
example : String
example = ?exampleTested on commit 1cf9849.
Thank you for Idris 2 :)
INTERNAL ERROR: Can't write resolved name
Steps to Reproduce
idris2 --check example.idr
EDIT: on commit 19a0795
interface Interface specifier where
0 concrete : specifier -> Type
record Value s where
constructor MkValue
specifier : s
0 DependentValue : Interface s => Value s -> Type
DependentValue v = concrete (specifier v)
-- Can't find an implementation for Interface s
-- record Record s where
-- constructor MkRecord
-- value : Value s
-- dependentValue : DependentValue {s} value
-- INTERNAL ERROR: Can't write resolved name 1102
data Record : s -> Type where
MkRecord : Value s -> DependentValue {s} value -> Record s
data Specifier = SBool | SString
implementation Interface Specifier where
concrete SBool = Bool
concrete SString = String
-- This is ok
0 TestSpecifier : Type
TestSpecifier = DependentValue (MkValue SBool)
t : TestSpecifier
t = TrueExpected Behavior
I'm probably doing something stupid but I was trying to get the a record work with a constrained interface, see above example for a simplified example.
Observed Behavior
The goal was to get the type of the dependentValue field in Record computed from the other value field and constrained by Interface.
The record was failing with Can't find an implementation for Interface s (which didn't really surprise me because the constraint is on the DependentValue, not the record, and I think there was some related limitations in Idris 1?).
So I tried to write the record without syntactic sugar as data but got this internal error.
Feel free to close the issue if can't do anything about it.
Undefined name
The program
module issues.UndefinedName
||| An isomorphism between two types
public export
record Iso a b where
constructor MkIso
to : a -> b
from : b -> a
toFrom : (y : b) -> to (from y) = y
fromTo : (x : a) -> from (to x) = x
||| Disjunction is commutative
public export
eitherComm : Iso (Either a b) (Either b a)
eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror where
{-
mirror : Either a' b' -> Either b' a'
mirror (Left x) = Right x
mirror (Right y) = Left y
---}
mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e
mirrorMirror (Left x) = Refl
mirrorMirror (Right x) = Refl
type checks in Idris 1 but not in Idris 2.
issues.UndefinedName> :r
1/1: Building issues.UndefinedName (issues/UndefinedName.idr)
issues/UndefinedName.idr:23:40--23:58:While processing right hand side of issues.UndefinedName.eitherComm at issues/UndefinedName.idr:17:1--26:1:
While processing type of 1161:mirrorMirror at issues/UndefinedName.idr:23:3--24:3:
Undefined name mirror
issues.UndefinedName>
I have no problem with the user having to provide an implementation of mirror, I was actually a bit surprised that Idris 1 can do without it! I am reporting the issue just in case Idris 2 is expected to behave as Idris 1 in this case.
Best way to add readline support?
I'm interested in helping to make the REPL better, in particular readline / history support. I'm wondering what your thoughts are about the best way to do this? I know of baseline-idris which FFI wraps readline, but if we use this, it would require installing both readline and baseline-idris as dependencies in order to build idris2. Any thoughts about other ways to do this, or should I just go ahead and use baseline-idris?
Add a way of running tests individually
Many tests are failing when I "make test", so I want to run a single test and manually compare its result with contents of the expected file. So I try this:
~/Desktop/Idris2-master/tests/idris2/basic011 $ sh ./run ../../../idris2
(implicit):1:1--1:1:Prelude not found
(implicit):1:1--1:1:Prelude not found
(implicit):1:1--1:1:Prelude not found
So I must be doing something wrong? Is this the correct way to try to run an individual test? Would be nice if there was some documentation for this.
Chez: Exception: variable make-thread-parameter is not bound
Steps to Reproduce
make install
Expected Behavior
All tests pass.
Observed Behavior
Chez tests return "Exception: variable make-thread-parameter is not bound".
Chez version: 9.5.3 (master from July 16th)
Can't find an implementation for Functor
The program
module issues.CannotFindImplementation
public export
interface Monad m => FooBar m where
Foo : {A : Type} -> A -> m A -> Type
bar : {A : Type} -> (ma : m A) -> m (DPair A (\ a => Foo a ma))
foobar : {A : Type} -> (ma : m A) -> map fst (bar ma) = ma
fails to type check in Idris2 with
issues.CannotFindImplementation> :r
1/1: Building issues.CannotFindImplementation (issues/CannotFindImplementation.idr)
issues/CannotFindImplementation.idr:10:40--10:57:While processing constructor issues.CannotFindImplementation.FooBar at issues/CannotFindImplementation.idr:3:1--13:1 at issues/CannotFindImplementation.idr:3:1--13:1:
Can't find an implementation for Functor m
issues.CannotFindImplementation>
The same error occurs if one replaces
interface Monad m => FooBar m where
with
interface Functor m => FooBar m where
The error message is triggered by map in the signature of foobar. It seems like an Idris2 bug to me given that map is a method of the Functor interface.
Proposal for FFI
I've recently been using the purescript FFI in anger and I have found it to be very nice to use. One of the main features of this style of FFI is that your code does not need to indicate the type of the underlying FFI. The examples given in purescript are javascript files but there is a C backend for purescript and you could write FFI code that would work in both with no changes, you only need to swap that the underlying *.js and *.c files that contain the appropriate function definitions.
I also think this could be developed in 2 stages, initially an FFI for chez could be implemented, this would likely be very simple to do since the RTS is chez and also because chez is dynamically typed. A second stage would be to implement a C FFI, this would require passing things through the chez ffi and will be more tricky to work out how to build and link and how best to deal with types, memory management etc. Chez has the tools for all this though so it will probably end up being more about how to deal with it in chez rather than how do deal with it in idris.
What do you think?
Can't have re-exporting modules
Steps to Reproduce
Foo.idr
module Foo
public export
foo : Nat -> Nat
foo = S
Bar.idr
module Bar
bar : String -> Nat
bar = length
Temp.idr
module Temp
import public Foo
import public Bar
temp.ipkg
package temp
modules = Foo
, Bar
, Temp
Expected Behavior
Everything compiles
Observed Behavior
$ idris2 --build temp.ipkg
1/3: Building Foo (Foo.idr)
2/3: Building Bar (Bar.idr)
Temp.idr:5:1--5:1:Parse error: Couldn't parse declaration (next tokens: [end of input])
High CPU/memory requirement compiling Vector indexing code
Steps to Reproduce
import Data.Vect
test : Vect 33 Int -> IO Int
test bytes_list = do
let int1 = (index 0 bytes_list * 8) + (index 1 bytes_list * 4) + (index 2 bytes_list * 2) + (index 3 bytes_list)
let int2 = (index 4 bytes_list * 8) + (index 5 bytes_list * 4) + (index 6 bytes_list * 2) + (index 7 bytes_list)
let int3 = (index 8 bytes_list * 8) + (index 9 bytes_list * 4) + (index 10 bytes_list * 2) + (index 11 bytes_list)
let int4 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
pure $ int1 + int2 + int3 + int4
Expected Behavior
Should compile quickly, nothing fancy here.
Observed Behavior
Seems to just hang at 100% CPU utilization. A previous version of this program triggered my OOM-killer...
Interestingly, if I remove two of the ints, it seems to compile. I tried compiling with gprof and using valgrind with the massif tool, but I can't figure out why the compiler gets stuck.
Can't use parent constraint in function
https://github.com/shmish111/Idris-Bifunctors/blob/master/Data/Bimonad.idr#L42
Steps to Reproduce
idris2 Data/Bimonad.idr
Expected Behavior
Type checks successfully
Observed Behavior
Data/Bimonad.idr:33:38--33:47:While processing right hand side of Data.Bimonad.Default implementation of >>== at Data/Bimonad.idr:33:3--41:1:
Can't find an implementation for Bifunctor p
Data/Bimonad.idr:42:15--42:25:While processing right hand side of Data.Bimonad.biunit at Data/Bimonad.idr:42:1--44:1:
Can't find an implementation for Biapplicative p
Data/Bimonad.idr:44:1--46:1:Undefined name Bimonad
If I explicitly add the Biapplicative p q constraint I get a different error that I don't understand at all:
Data/Bimonad.idr:33:38--33:47:While processing right hand side of Data.Bimonad.Default implementation of >>== at Data/Bimonad.idr:33:3--41:1:
Can't find an implementation for Bifunctor p
Data/Bimonad.idr:41:11--41:28:While processing type of Data.Bimonad.biunit at Data/Bimonad.idr:41:1--42:1:
When unifying Type and (Type -> Type -> Type) -> ?a
Mismatch between:
Type
and
(Type -> Type -> Type) -> ?a
Data/Bimonad.idr:42:1--44:1:No type declaration for Data.Bimonad.biunit
Data/Bimonad.idr:44:1--46:1:Undefined name Bimonad
Auto-search is slow when restricting a heterogenous list to a predicate type
(I initially wrote this as a comment on a closed issue, but I think it makes more sense to add a new issue. Sorry about that.)
It unfortunately seems like the patch for #25 reduces the performance of some uses of auto-search.
After updating my Erlang codegen-branch to include all changes from Idris 2's master branch, I noticed that the Erlang module would not finish type-checking. I found that the change in performance happened specifically in the commit edwinb/Idris2@677ddea ("Only check determining arguments at the top level").
The Erlang module include functions (e.g. erlCall) that require a proof that its arguments only consist of types that have a mapping to Erlang. These types are specified in a predicate type called ErlType a.
Steps to Reproduce
I have reduced the Erlang module to the following code, that still exhibit the problem:
data ErlList : List Type -> Type where
Nil : ErlList []
(::) : x -> ErlList xs -> ErlList (x :: xs)
data ErlType : Type -> Type where
ETInteger : ErlType Integer
ETString : ErlType String
data ErlTypes : List Type -> Type where
ETErlTypesNil : ErlTypes []
ETErlTypesCons : (ErlType x, ErlTypes xs) => ErlTypes (x :: xs)
erlCall : ErlList xs -> {auto prf : ErlTypes xs} -> ()
erlCall args = ()
foo : ()
foo = erlCall [1, 2, 3]
(I kept the original names of the types/functions to make it easier to cross-reference the code in the Erlang module.)
Expected Behavior
Timings when type-checking this sample program with different amount of arguments to erlCall:
Args to erlCall |
Before patch |
|---|---|
| [] | 0.08s |
| [1] | 0.09s |
| [1, 2] | 0.09s |
| [1, 2, 3] | 0.09s |
| [1, 2, 3, 4] | 0.10s |
Observed Behavior
Timings when type-checking this sample program with different amount of arguments to erlCall:
Args to erlCall |
After patch |
|---|---|
| [] | 0.08s |
| [1] | 2.17s |
| [1, 2] | 5.16s |
| [1, 2, 3] | 7.98s |
| [1, 2, 3, 4] | 10.50s |
Can't build network library on Windows
Using Idris 1.3.2, and msys64, on Windows 10.
I was able to resolve the issues in https://github.com/edwinb/Idris2/issues/41, but now I'm getting stuck on the make network step, after completing make idris2, make prelude and make base.
C:\Users\joshua.hillerup\Source\Idris\Idris2>make network
make -C libs/prelude IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
../../idris2 --build prelude.ipkg
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
make -C libs/network IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cc -c -o idris_net.o idris_net.c
cc -o idris_net.so -shared idris_net.o -lws2_32
creating 'build' directory
../../idris2 --build network.ipkg
1/3: Building Network.Socket.Data (Network/Socket/Data.idr)
2/3: Building Network.Socket.Raw (Network/Socket/Raw.idr)
3/3: Building Network.Socket (Network/Socket.idr)
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make -C libs/network test IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cp idris_net.so libidris_net.so # to make C linker happy
cc -o network-tests -L. -I. test.c -lidris_net
test.c:3:10: fatal error: netinet/in.h: No such file or directory
3 | #include <netinet/in.h>
| ^~~~~~~~~~~~~~
compilation terminated.
make[1]: *** [Makefile:52: test] Error 1
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make: *** [Makefile:31: network] Error 2
Note: I do have netinet\in.h in my path, it's the first path entry even just to be sure.
Also, I added the -lws2_32 switch myself. Without it it fails earlier, with this error:
C:\Users\joshua.hillerup\Source\Idris\Idris2>make network
make -C libs/prelude IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
../../idris2 --build prelude.ipkg
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
make -C libs/network IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cc -c -o idris_net.o idris_net.c
cc -o idris_net.so -shared idris_net.o
idris_net.o:idris_net.c:(.text+0xb): undefined reference to `__imp_WSACleanup'
idris_net.o:idris_net.c:(.text+0x39): undefined reference to `__imp_WSAStartup'
idris_net.o:idris_net.c:(.text+0xa5): undefined reference to `__imp_htonl'
idris_net.o:idris_net.c:(.text+0x121): undefined reference to `__imp_ntohl'
idris_net.o:idris_net.c:(.text+0x1cf): undefined reference to `__imp_socket'
idris_net.o:idris_net.c:(.text+0x25b): undefined reference to `__imp_getaddrinfo'
idris_net.o:idris_net.c:(.text+0x27c): undefined reference to `__imp_getaddrinfo'
idris_net.o:idris_net.c:(.text+0x2ed): undefined reference to `__imp_bind'
idris_net.o:idris_net.c:(.text+0x337): undefined reference to `__imp_getsockname'
idris_net.o:idris_net.c:(.text+0x380): undefined reference to `__imp_getsockname'
idris_net.o:idris_net.c:(.text+0x3b9): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x3d4): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x44f): undefined reference to `__imp_connect'
idris_net.o:idris_net.c:(.text+0x468): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x47f): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x4f6): undefined reference to `__imp_inet_ntop'
idris_net.o:idris_net.c:(.text+0x52a): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x585): undefined reference to `__imp_accept'
idris_net.o:idris_net.c:(.text+0x5ca): undefined reference to `__imp_send'
idris_net.o:idris_net.c:(.text+0x657): undefined reference to `__imp_send'
idris_net.o:idris_net.c:(.text+0x6dd): undefined reference to `__imp_recv'
idris_net.o:idris_net.c:(.text+0x74c): undefined reference to `__imp_recv'
idris_net.o:idris_net.c:(.text+0x87e): undefined reference to `__imp_sendto'
idris_net.o:idris_net.c:(.text+0x891): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x933): undefined reference to `__imp_sendto'
idris_net.o:idris_net.c:(.text+0xa12): undefined reference to `__imp_recvfrom'
idris_net.o:idris_net.c:(.text+0xb0e): undefined reference to `__imp_recvfrom'
idris_net.o:idris_net.c:(.text+0xbea): undefined reference to `__imp_ntohs'
collect2.exe: error: ld returned 1 exit status
make[1]: *** [Makefile:39: idris_net.so] Error 1
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make: *** [Makefile:30: network] Error 2
can't construct pair using applicative
https://gist.github.com/shmish111/0172215916669ae9f5ef822ffcc7c429
Steps to Reproduce
idris2 D.idr
Expected Behavior
Type checks successfully
Observed Behavior
D.idr:4:39--8:1:While processing right hand side of D.func1 at D.idr:4:1--8:1:
When unifying f d and f d
When unifying f (d -> ?b) and f ((1 y : ?b) -> (c, ?b))
Mismatch between:
d -> ?b
and
(1 y : ?b) -> (c, ?b)
Note that func2 in the gist checks just fine so it's something about applying the linear function Builtin.MkPair : (1 x : a) -> (1 y : b) -> (a, b)
Also if I use holes
func1 f g (a, b) = MkPair <$> ?first <*> ?second
I get the type of ?first as
Idris: Type of first
0 d : Type
0 b : Type
0 c : Type
0 a : Type
0 f : Type -> Type
conArg : Applicative f
b : b
a : a
g : b -> f d
f : a -> f c
-------------------------------------
first : f c
No mention of the quantity requirement.
Using Data.Vect.index too expensive (maybe Fin problem?)
Steps to Reproduce
On commit 56a09b0
module TooSlow
import Data.Vect
test : Vect 1 () -> IO ()
test b = do
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
let i = index 1 b
pure ()
main : IO ()
main = do
pure ()
Expected Behavior
Should compile and run quickly.
Observed Behavior
Needs more than 10 seconds to compile, don't know how long it would need.
Enable CI
The CI configuration is in place, so PRs should run through CI once @edwinb toggles the switch to build this project at https://travis-ci.org/account/repositories.
Can't solve constraint
The program
module issues.CannotSolveConstraint
import Data.Fin
import Data.Vect
public export
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
public export
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
public export
toVectRepr : {A : Type} -> (f : Fin n -> A) -> (k : Fin n) -> index k (toVect f) = f k
toVectRepr {n = Z} f k = absurd k
toVectRepr {n = S m} f FZ = Refl
toVectRepr {n = S m} f (FS k) = toVectRepr (tail f) k
type checks fine in Idris 1 but not in Idris 2:
1/1: Building issues.CannotSolveConstraint (issues/CannotSolveConstraint.idr)
issues/CannotSolveConstraint.idr:18:33--19:1:While processing right hand side of issues.CannotSolveConstraint.toVectRepr at issues/CannotSolveConstraint.idr:18:1--19:1:
Can't solve constraint between:
index FZ (toVect f)
and
f FZ
issues.CannotSolveConstraint>
The implementation of index is the same in Idris1 and Idris 2. But in Idris 1 the export modifier of indexis public export whereas in Idris 2 it is just export.
Is this the reason why Idris 2 fails to type check toVectRepr? Why is the export modifier of index different in Idris 1 and Idris 2?
Error with type-level type-annotated let expression
Steps to Reproduce
Run idris2 fail.idr
where the file fail.idr is:
data A : Type where
The : Type -> A
U : A -> Type
U (The x) = x
works : (a : A) -> (H : U a) -> (let q = H in Nat)
works a h = 0
fails : (a : A) -> (H : U a) -> (let q : U a = H in Nat)
fails a h = 0
Expected Behavior
$ idris2 fails.idr
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main>
Observed Behavior
$ idris2 fails.idr
1/1: Building fails (fails.idr)
fails.idr:11:48--11:50:While processing type of Main.fails at fails.idr:11:1--12:1:
While processing type of 1080:q at fails.idr:11:38--11:50:
Can't solve constraint between:
U a
and
Type
fails.idr:12:1--13:1:No type declaration for Main.fails
A related file that does work is works.idr:
U : Type -> Type
U x = x
works : (a : Type) -> (H : U a) -> (let q = H in Nat)
works a h = 0
fails : (a : Type) -> (H : U a) -> (let q : U a = H in Nat)
fails a h = 0
Can't find an implementation
The program
import Control.Monad.Identity
public export
interface Foo (sA : Type) where
A : Type
Elem : A -> sA -> Type
Empty : sA -> Type
Empty as = (a : A) -> Not (Elem a as)
public export
implementation Foo (Identity Bool) where
A = Bool
Elem x (Id y) = x = y
fails to type check with
nicola@lt561:~/gitlab/botta/Idris2Libs$ idris2 issues/CannotFindImplementation1.idr
1/1: Building issues.CannotFindImplementation1 (issues/CannotFindImplementation1.idr)
issues/CannotFindImplementation1.idr:10:1--18:1:While processing right hand side of Main.Empty at issues/CannotFindImplementation1.idr:10:1--18:1:
Can't find an implementation for Foo ?sA
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main>
The program can be made to type check by commenting out the implementation of Empty in the Foo interface. This seems like an Idris 2 bug to me: the expected behavior would be that the program type checks.
Implicit lambda arguments
(This is more of a feature request, but it's been a long-standing stumbling block for me in Idris 1, and I hope it's fairly uncontroversial)
Steps to Reproduce
module Temp
import Data.Vect
All : (a : i -> Type) -> Type
All a {i} = {j : i} -> a j
Vect' : Type -> Nat -> Type
Vect' = flip Vect
infixr 1 :->
(:->) : (a, b : i -> Type) -> (i -> Type)
(:->) a b i = a i -> b i
showAll : All (Vect' Integer :-> Vect' String)
showAll = map show
justShowAll : Maybe (All (Vect' Integer :-> Vect' String))
justShowAll = Just ?hole
Expected Behavior
justShowAll = Just $ \{j} => map show
Observed Behavior
There doesn't seem to be a way to introduce the implicit to finish filling the hole.
`integerToNat` hangs for negative integers
Steps to Reproduce
integerToNat (2 - 3)
Expected Behavior
Either return Z or throw an error
Observed Behavior
non terminating loop (well it will probably fail eventually when it gets to the last negative integer)
Extra Info
I came across this because I am working on a project where we want to use natural numbers in both Haskell and Purescript. It turns out that Haskell natural numbers libraries all implement Num which in haskell has methods for negate and -. This means that the library authors chose a certain behaviour (crashing in most cases) in order to get + and *.
In purescript + and * are part of the Semiring class which is much nicer. There is an integerToNat function defined in Data.Natural but it's not part of any standard class because it makes a choice as to what should happen. Similarly there is also a minus function that is not part of any class for the same reason.
It seems to me that the way numeric classes work in Purescript is very well thought out and I've now come across a situation where that matters. Could we copy these numeric classes in Idris2 rather than the current classes (Num, Neg etc), they seem a little more standard in terms of it is clear what a Semiring is, there are agreed upon rules, the same can't be said for Num, for example it is quite different in Haskell and Idris.
So finally there should either be no integerToNat defined or it should either crash or return Z or possibly have 2 different versions that do different things. Nat should not implement a class that has fromInteger though.
Can't build on Windows using Idris 1.3.2
I just updated to Idris 1.3.2 using the Windows binary. I don't think this is related to the Chez Scheme problem, because it didn't get anywhere close to running tests.
Here is what's in the command line, running on Windows 10, on a system where I have successfully built smaller Idris 1 projects:
Microsoft Windows [Version 10.0.18362.239]
(c) 2019 Microsoft Corporation. All rights reserved.
C:\Users\zente\Documents\Idris\Idris2>make idris2
idris --build idris2.ipkg
Entering directory `.\src'
Type checking .\Core\Context.idr
.\Core\Context.idr:26:13-35:15:
|
26 | PMDef : (alwaysReduce : Bool) -> -- always reduce, even when quoting etc
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking type of Core.Context.PMDef:
No such variable CaseTree
.\Core\Context.idr:60:1-8:
|
60 | Show Def where
| ~~~~~~~~
When checking type of Core.Context.Def implementation of Prelude.Show.Show:
When checking argument ty to type constructor Prelude.Show.Show:
No such variable Def
.\Core\Context.idr:155:1-175:26:
|
155 | public export
| ~~~~~~~~~~~~~ ...
When checking type of Core.Context.MkGlobalDef:
No such variable Def
make: *** [Makefile:12: idris2] Error 1
C:\Users\zente\Documents\Idris\Idris2>idris --version
1.3.2
C:\Users\zente\Documents\Idris\Idris2>
can't infer type in where clause
See https://gist.github.com/shmish111/02b71edf3e289bcc2ee9f48d55aac86f
Steps to Reproduce
idris C.idr
Expected Behavior
Module compiles
Observed Behavior
C.idr:7:9--7:17:While processing right hand side of C.f at C.idr:4:1--7:17:
No type declaration for C.f'
I'm not sure if this is expected or not but it's at least a "type inference regression" from Idris 1 😢
Mismatch: expected behaviour?
The program
module issues.Mismatch
interface Monad m => FooBar m where
Foo : {A : Type} -> A -> m A -> Type
Bar : {A : Type} -> m A -> Type
foo : {A : Type} -> (a : A) -> (ma : m A) -> Foo a ma -> Bar ma
fails to type check with
issues.Mismatch> :r
1/1: Building issues.Mismatch (issues/Mismatch.idr)
issues/Mismatch.idr:9:3--12:1:While processing right hand side of issues.Mismatch.foo at issues/Mismatch.idr:9:3--12:1:
When unifying __bind_Bar arg and Bar ma
Mismatch between:
A
and
{A:222}
issues.Mismatch>
The issue can be solved by replacing
foo : {A : Type} -> (a : A) -> (ma : m A) -> Foo a ma -> Bar ma
with
foo : {A : Type} -> (a : A) -> (ma : m A) -> Foo a ma -> Bar {A} ma
I am not sure whether this is an Idris2 bug or the expected behaviour, it seems to me that the type checker should be able to deduce the value of the implicit argument of Bar in this case.
Cycle detected in solution of metavariable:
I am not sure how to reproduce this in a small, self-contained example but you should be able to download https://gitlab.pik-potsdam.de/botta/Idris2Libs and then do:
idris2 FiniteAsSigmaType/Properties.idr
in the root directory of Idris2Libs. This should work fine. However, doing
idris2 FiniteAsInterface/Properties.idr
should yield
14/16: Building FiniteAsInterface.Finite (FiniteAsInterface/Finite.idr)
15/16: Building FiniteAsInterface.Operations (FiniteAsInterface/Operations.idr)
16/16: Building FiniteAsInterface.Properties (FiniteAsInterface/Properties.idr)
FiniteAsInterface/Properties.idr:24:16--24:35:While processing right hand side of FiniteAsInterface.Properties.toVectComplete at FiniteAsInterface/Properties.idr:23:1--34:1:
While processing type of 2356:s1 at FiniteAsInterface/Properties.idr:24:3--25:3:
Sorry, I can't find any elaboration which works. All errors:
If Fin.Operations.toVect: Cycle detected in solution of metavariable $resolved2372
If FiniteAsInterface.Operations.toVect: Cycle detected in solution of metavariable $resolved2372
Welcome to Idris 2 version 0.0. Enjoy yourself!
FiniteAsInterface.Properties>
This is strange because the type of s1 in FiniteAsInterface.Properties.toVectComplete is the same as the type of s1 in FiniteAsSigmaType.Properties.toVectComplete.
If you think it's worth, I can try to build a self-contained example of this behavior.
Idris 2 should compile itself
This is well a general discussion about what is needed for bootstraping Idris 2.
idea: monolithic executables with chez-exe
see gwatt/chez-exe
Would it be neat to be able to "compile" idris2 programs to monolithic executables (by bundling the idris2 runtime/libraries and the user's script/packages and chez scheme)?
Creating this issue in case there is interest, to be studied in the future
Not a valid implicit argument
The program
module Implementation
import Data.Fin
interface Foo t where
foo : Nat
implementation Foo (Fin n) where
foo {n} = n
type checks fine in Idris but not in Idris 2:
nicola@lt561:~/gitlab/botta/Idris2Libs/issues$ idris2 Implementation.idr
1/1: Building Implementation (Implementation.idr)
Implementation.idr:9:3--9:11:While processing left hand side of Implementation.foo at Implementation.idr:9:3--10:1:
n is not a valid implicit argument in foo
Welcome to Idris 2 version 0.0. Enjoy yourself!
Infinite loop in the REPL for GenerateDefinition on binary tree
The REPL seems to be able to generate the definition for specialized linear map definition for List, but if we add a second recursive parameter (such as required for a binary tree), then generate definition loops forever.
Steps to Reproduce
Please see https://gist.github.com/vladciobanu/a9509be6e005312af698a03d324cc0d9 for a trivial reproduction example. The code includes the List version to showcase the differences.
Expected Behavior
Generate the correct implementation, or at least report it can't.
Observed Behavior
Infinite loop.
Possibly related, but unsure. Let me know if I should create a different issue for this.
If I change the definition of Tree to
data Tree a = TNil | Node a (List' (Tree a))
mapTree : ((1 x : a) -> b) -> (1 t : Tree a) -> Tree band try to generate its map function, I get:
mapTree f TNil = TNil
mapTree f (Node x y) = mapTree f (Node x (Cons TNil y))If I change the definition to
data Tree a = NNode a (List' (Tree a))Then it reports it can't find a definition for the same mapTree, although we can write:
mapTree f (Node x xs) = Node (f x) (mapList (mapTree f) xs)Idris freezes when trying to implement Biapplicative Pair
https://github.com/shmish111/Idris-Bifunctors/blob/master/Data/Biapplicative.idr#L67
Steps to Reproduce
replace line 68 with a *>> b = bimap (const id) (const id) <<$>> a <<*>> b
run idris2 Data/Biapplicative.idr
Expected Behavior
Type checking completes and repl loads
Observed Behavior
idris2 process freezes
I've tried to work out which part is causing the issue but I couldn't. I was also unsure how to go about debugging idris2?
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.