5 ms·

> dependent types are used to encode logic's quantifiers like "for all" and "there exists" Ya I don't think this is a good definition of dependent type - the p

> dependent types are used to encode logic's quantifiers like "for all" and "there exists" 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. Obviously there's a mapping from what you wrote to this (in the same way there's almost always a mapping from a sequence of decision problems to an optimization problem) but it's still not a good formulation. > In my example the objects could be any object types, combination of types, or concepts Um yes this is literally what I was asking with respect to top ⊤. > usually can't [contain] expressions ya the negation is interesting - I wonder how it's implemented.

elcritch 3y ago
> 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 https://github.com/elcritch/platonic 2: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
- mathisfun123 3y ago
  > Nim's VM runs from Nim AST What does this mean? There's a runtime VM or compile time VM?
  - elcritch 3y ago
    > 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 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.
    - mathisfun123 3y ago
      ah so like clang's constexpr. got it. thanks
- deleted 3y ago
  [deleted]
elcritch 3y ago
P.S. I went through Wikipedia's definition a bit more. Not sure it's a full dependent types with the type pairs and stuff. Nim does let you do (constant) value to type conversion with expressions: https://play.nim-lang.org/#ix=4HRz https://play.nim-lang.org/#ix=4HRz or more oddly https://play.nim-lang.org/#ix=4HRA https://play.nim-lang.org/#ix=4HRA . That'd seem to satisfy the `Π` definition and lack of fixed codomain. Though I've never taken a set theory course so YMMV.

elcritch 3y ago

> 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 https://github.com/elcritch/platonic 2: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html

mathisfun123 3y ago
> Nim's VM runs from Nim AST What does this mean? There's a runtime VM or compile time VM?
- elcritch 3y ago
  > 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 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.
  - mathisfun123 3y ago
    ah so like clang's constexpr. got it. thanks
deleted 3y ago
[deleted]

elcritch 3y ago

P.S. I went through Wikipedia's definition a bit more. Not sure it's a full dependent types with the type pairs and stuff. Nim does let you do (constant) value to type conversion with expressions: https://play.nim-lang.org/#ix=4HRz https://play.nim-lang.org/#ix=4HRz or more oddly https://play.nim-lang.org/#ix=4HRA https://play.nim-lang.org/#ix=4HRA . That'd seem to satisfy the `Π` definition and lack of fixed codomain. Though I've never taken a set theory course so YMMV.