Our great sponsors
-
-
Nim
Nim is a statically typed compiled systems programming language. It combines successful concepts from mature languages like Python, Ada and Modula. Its design focuses on efficiency, expressiveness, and elegance (in that order of priority).
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
As recommended by michaelsbradley below, I installed https://github.com/nim-lang/langserver. I'm using coc.nvim (https://github.com/neoclide/coc.nvim) so I followed the instructions here from nim langserver https://github.com/nim-lang/langserver#vimneovim and seems to be working well!
You may fare better hooking VSCode to nimlangserver:
https://github.com/saem/vscode-nim#nim-lanugage-server-integ...
> Ya I don't think this is a good definition of dependent type - the prototypical example of a dependent type is a k-length vector.
Yah that's why I qualified my statement as dependent type like setup as I don't know a good definition of dependent types which I really grok and I've only briefly dabbled in it. It'd be awesome if you could point out a good resource showing a clear example / simple proof.
Well I started working on statically typed vector concepts [1]. The compiler can't do `proc concat[N,M: static int](v1: Vector[N], v2: Vector[M}): Vector[N+M]` and it fails. It might be able to be implemented via a macro like `proc concat(v1: Vector[N], v2: Vector[M}): typeFromSumOf(N,M)`, but I haven't tried yet.
Also just using static ints would require specific values at some point to work I think. Whereas you'd really want "induction" of some sort. Maybe a SAT solver would be required at that point? There's DrNim [2] which does tie Z3 but it's sorta dormant.
> Um yes this is literally what I was asking with respect to top ⊤.
Ah, I didn't know what you meant by top T.
> ya the negation is interesting - I wonder how it's implemented.
Nim's VM runs from Nim AST, so probably running it as a VM expression.
1: https://github.com/elcritch/platonic
> What does this mean? There's a runtime VM or compile time VM?
Compile time VM. It's used to run macros / templates / concepts. You can also run most code at compile time in a `static` block except for stuff that needs C calls. You can also compile the VM into a program and use it as a runtime VM (see https://github.com/beef331/nimscripter) which I do in my GUI lib. NIR should enable the compile time VM to run faster too, and possibly use JIT'ed code.
Downloading https://github.com/PMunch/nimlsp using git
As recommended by michaelsbradley below, I installed https://github.com/nim-lang/langserver. I'm using coc.nvim (https://github.com/neoclide/coc.nvim) so I followed the instructions here from nim langserver https://github.com/nim-lang/langserver#vimneovim and seems to be working well!
There has been a more-or-less working CPS implementation for Nim for a few years now,
https://github.com/nim-works/cps
https://github.com/nim-works/cps/tree/master/docs
Nobody seems to care though, as it has gained no traction at all and it has been mostly ignored by the core team.