4 ms·

I'm feeling both really pissed and validated right now. I thought this was going to just be a normal thoughtless config language that would only be successful a

by wlib 7y ago

I'm feeling both really pissed and validated right now. I thought this was going to just be a normal thoughtless config language that would only be successful as a Google project. Then I looked at the theoretical basis page. I have no formal proof about this, but I've been talking about this type of a type system with my parents and high school CS teacher for a while now! My idea sounds like this: a value is simply an actual binary string. The "type" that classifies any data is described as a formal grammar, where the binary string is a formal language. If the language can parse a given binary value with the formal grammar, that value is an element of the set (type). This naturally leads to a structural type system which can be described using existing set theory and implemented using existing parsers and formal language theory. Of course, this leads to type -> type functions which describe dependent and refinement types naturally. It's great to see this idea being broadcast on the front page here, as I can see it very clearly as a superior type system. I'm really regretting not writing a formal article about it sooner!

uryga 7y ago
> Of course, this leads to type -> type functions which describe dependent and refinement types naturally. could you expand on this? i don't understand how you get this from grammars. (on a side note, i think that dependent types usually mean you can write functions from values to types, not type -> type?)
- wlib 7y ago
  Yes, I mistyped that bit. I meant to say that because types (as a grammar) are values, they can be inputs and outputs of functions. The functions can fill in the hole that dependent/refinement types fill, by taking context into account (the grammars which describe simple types being context free). Type -> Type fill in for type constructors like this infinite list: InfiniteListOf = Type -> Type & InfiniteListOf Type That function just morphs a simple grammar into another grammar. Imagine now if we could calculate something in between: IncrementingInfiniteListFrom = number -> number & IncrementingInfiniteListFrom number+1 That's where the dependent types come in, naturally.
emmanueloga_ 7y ago
Why feeling pissed? It is unlikely this Cue project implements the very same semantics the way you think about them. I'd go ahead and just write that paper. Looking forward seeing your reference implementation :-).

by wlib 7y ago

uryga 7y ago

> Of course, this leads to type -> type functions which describe dependent and refinement types naturally. could you expand on this? i don't understand how you get this from grammars. (on a side note, i think that dependent types usually mean you can write functions from values to types, not type -> type?)

wlib 7y ago
Yes, I mistyped that bit. I meant to say that because types (as a grammar) are values, they can be inputs and outputs of functions. The functions can fill in the hole that dependent/refinement types fill, by taking context into account (the grammars which describe simple types being context free). Type -> Type fill in for type constructors like this infinite list: InfiniteListOf = Type -> Type & InfiniteListOf Type That function just morphs a simple grammar into another grammar. Imagine now if we could calculate something in between: IncrementingInfiniteListFrom = number -> number & IncrementingInfiniteListFrom number+1 That's where the dependent types come in, naturally.

emmanueloga_ 7y ago

Why feeling pissed? It is unlikely this Cue project implements the very same semantics the way you think about them. I'd go ahead and just write that paper. Looking forward seeing your reference implementation :-).