Ceylon type system is Chomsky-3-complete

[Lucas Werkmeister]

I’m pretty sure I’ve found a way to convert any finite state automaton into a series of Ceylon definitions, and any word into a Ceylon statement, so that the statement is well-typed (i. e., compiles) if, and only if, the word is accepted by the automaton.
Thus, the Ceylon type system / typechecker is Chomsky-3-complete.

I just thought I’d let you know, because this is obviously vital to the success of the Ceylon platform and whatnot :D

Example here: https://github.com/lucaswerkmeister/ceylon-typesystem-chomsky-3/blob/master/source/tmp/run.ceylon
accepts the language  x1*x2⁺
(More or less) formal/conclusive proof following soon!


Challenge: I suspect that with tuple types, it might even be possible to implement a nondeterministic pushdown automaton, which is Chomsky-2 (aka context-free languages, e. g. the language of correct bracket terms).

[Gavin King]

What does this mean, precisely? That you can encode a regular
expression into the type system, and use the typechecker as a
recognizer?

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-users...@googlegroups.com.
> To post to this group, send email to ceylon...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ceylon-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ceylon-users/47ce9cf4-9d8e-4516-b3de-b5aa61709ecc%40googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.



--
Gavin King
ga...@ceylon-lang.org
http://profiles.google.com/gavin.king
http://ceylon-lang.org
http://hibernate.org
http://seamframework.org

[Lucas Werkmeister]

hat you can encode a regular
expression into the type system, and use the typechecker as a
recognizer?

Exactly. (Only true regular expressions though, not insanely complex regexes with lookbehind and stuff like that.)
 

[Gavin King]

On Wed, Feb 19, 2014 at 11:28 AM, Lucas Werkmeister
<lucas.we...@googlemail.com> wrote:
>> hat you can encode a regular
>> expression into the type system, and use the typechecker as a
>> recognizer?
>
>
> Exactly. (Only true regular expressions though, not insanely complex regexes
> with lookbehind and stuff like that.)

Sure that's what I meant.

And is this something that is generally possible in most type systems?
Or is it generally not possible?

[Lucas Werkmeister]

I don’t think it’s possible in type systems without union and intersection types. At least, I can’t think of a way to do it without them – I used union types to combine the multiple state transitions into a single function, and intersection types to select a single state and input character per transition: “If we’re in Q1 and get the character x1, the next state is Q2” is encoded as S&Q1&C&X1&B<Q2> (where S and C are type parameters for the input state and character, and B is a “box” around a type to avoid piling more and more intersections onto the type).

[Gavin King]

Interesting.

On Wed, Feb 19, 2014 at 12:05 PM, Lucas Werkmeister
<lucas.we...@googlemail.com> wrote:
> I don't think it's possible in type systems without union and intersection

> types. At least, I can't think of a way to do it without them - I used union

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-users...@googlegroups.com.
> To post to this group, send email to ceylon...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ceylon-users.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ceylon-users/19870283-1cec-4b44-a940-6c9cc57b63bf%40googlegroups.com.

>
> For more options, visit https://groups.google.com/groups/opt_out.

[Ross Tate]

Yo Dexter,

You know all about regular expressions and Kleene algebras. Ceylon has union and intersection types, and Lucas thinks he's found a way to use those to encode regular expressions in Ceylon's type system. Does this seem reasonable to you, and do you know of any other fun related connections? I'm happy to chat with you offline to catch you up on the type system.

- Ross

--

You received this message because you are subscribed to the Google Groups "ceylon-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/47ce9cf4-9d8e-4516-b3de-b5aa61709ecc%40googlegroups.com.

[Lucas Werkmeister]

I’ve added a second example to the repository that checks if a number is not divisible by three.
For example, this is well-typed:

Accept q = t(t(t(t(t(initial, _1), _6), _7), _3), _5);

but this isn’t:

Accept q = t(t(t(t(t(initial, _1), _6), _7), _3), _4);

This is probably a much better demonstration of the capabilities of the Ceylon type system.
(Divisibility by other natural numbers is also regular, but the automaton gets uglier.)

The repository also contains an attempt at a formal-ish proof (LaTeX).

Next, I’ll try to implement a stack in the type system (should be possible similar to Tuple). If that works, then there’s no reason why two stacks shouldn’t work – but a two-stack pushdown automaton is Turing complete! Stay tuned.

[Lucas Werkmeister]

I seem to have run into some issues with multi-level generics, and I’m not sure if they’re bugs or legitimate limitations.

void test<R, I>(R r)
        given I satisfies Integer
        given R satisfies Range<I> // type parameter Element of declaration Range has argument I not assignable to upper bound Ordinal<I> of Element
        {}

A Range<Integer> is obviously perfectly legal.
Is this correct, or a bug?

[Gavin King]

On Fri, Feb 21, 2014 at 2:23 PM, Lucas Werkmeister
<lucas.we...@googlemail.com> wrote:
> I seem to have run into some issues with multi-level generics, and I'm not
> sure if they're bugs or legitimate limitations.
> void test<R, I>(R r)
> given I satisfies Integer
> given R satisfies Range<I> // type parameter Element of declaration
> Range has argument I not assignable to upper bound Ordinal<I> of Element
> {}
> A Range<Integer> is obviously perfectly legal.
> Is this correct, or a bug?

Looks right to me. Just because I is an Ordinal<Integer> doesn't mean
it's an Ordinal<I>.

[Lucas Werkmeister]

I can’t quite get the stack to work. I’ve pushed again to the WIP branch (here), if any of you typesystem wizards want to look at it, go ahead :)

[Gavin King]

Yes, it infers Nothing. Which looks correct to me, I don't see any
constraint that should be lowerbounding RestStack.

On Fri, Feb 28, 2014 at 1:00 PM, Lucas Werkmeister

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-users...@googlegroups.com.
> To post to this group, send email to ceylon...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ceylon-users.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ceylon-users/ffb6893d-5805-47d8-adb1-407469817ce8%40googlegroups.com.

>
> For more options, visit https://groups.google.com/groups/opt_out.