Ancestors

Toot

Written by Edwin Brady on 2024-11-06 at 00:19

I often read on the Internet - and I realise that I should know by now that it's not a good place to read things - that Idris isn't Turing Complete and can't be because it's dependently typed. I think I can guess where this idea comes from, but, in case of any doubt, it's Turing Complete. Of course it's Turing Complete. For goodness sake...

=> More informations about this toot | More toots from edwinb@types.pl

Descendants

Written by Edwin Brady on 2024-11-06 at 00:21

I once implemented Whitespace in Idris because I was the right sort of bored. People are happy to believe Whitespace is Turing Complete but Idris? No, couldn't possibly be, I mean it's dependently typed isn't it? (Of course it is. Stop it.)

=> More informations about this toot | More toots from edwinb@types.pl

Written by Edwin Brady on 2024-11-06 at 00:24

Turing Completeness is overrated anyway. Pacman Completeness is where it's at.

=> More informations about this toot | More toots from edwinb@types.pl

Written by Irenes (many) on 2024-11-06 at 00:19

@edwinb ah wow. yeah, sorry you have to deal with that.

=> More informations about this toot | More toots from ireneista@irenes.space

Written by Edwin Brady on 2024-11-06 at 00:21

@ireneista these days I just ignore it because it's hardly worth it.

=> More informations about this toot | More toots from edwinb@types.pl

Written by Irenes (many) on 2024-11-06 at 00:23

@edwinb we're glad you're able to, and we agree with that conclusion

=> More informations about this toot | More toots from ireneista@irenes.space

Written by Thomas on 2024-11-06 at 04:39

@edwinb Tetris Complete is also a concept I've used when discussing expressive power

=> More informations about this toot | More toots from tfb@functional.cafe

Written by chris martens on 2024-11-27 at 13:00

@edwinb this is a pin-worthy toot (i say, having gone looking for it nearly a month after the fact)

=> More informations about this toot | More toots from chrisamaphone@hci.social

Written by Edwin Brady on 2024-11-27 at 13:06

@chrisamaphone That hadn't occurred to me, but yes I think it probably is isn't it?

=> More informations about this toot | More toots from edwinb@types.pl

Written by Tristram Brelstaff on 2024-11-28 at 18:18

@edwinb Admit it: you only say that because Pacman completeness is much more fun to test than Turing completeness!

=> More informations about this toot | More toots from tristrambrelstaff@mathstodon.xyz

Written by Dani ✨🐚 on 2024-11-06 at 00:58

@edwinb magic: the gathering confirmed no longer turing complete thanks to introduction of dependently typed planeswalkers

=> More informations about this toot | More toots from danielle@types.pl

Written by Chris Lam on 2024-11-06 at 08:41

@edwinb My impression was that you can have a Turing complete dependently typed language but your logic becomes unsound along the way

=> More informations about this toot | More toots from clam@mathstodon.xyz

Written by Artem Pelenitsyn on 2024-11-06 at 01:26

@edwinb "Idris is not Turing-complete because it's dependently-typed" sounds like something that ChatGPT would tell you

=> More informations about this toot | More toots from artem@functional.cafe