> I don't get it - if empty object doesn't act as a top how does what you wrote demonstrate flexibility?
To quote from Wikipedia:
dependent types are used to encode logic's quantifiers like "for all" and "there exists". ... dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations
In my example the objects could be any object types, combination of types, or concepts. It allows you to encode logic at the type system level. If you use generics with the example above you can do things roughly like:
type
State = enum Open, Closed
SomeObject[T: State] = object
val: int
SomeObjectOpen = not SomeObject[state.Close]
proc close(obj: SomeObjectOpen) = ...
You can do some simlar things in other languages, but it's hard and more limited and usually can't expressions.
> 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.
> 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.
> 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.
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 or more oddly 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.
