/sci/ - Science & Math » Thread #11270046

276KiB, 1280x720, caption_blank.jpg

View Same Google iqdb SauceNAO

Markov's principle

Anonymous Wed 01 Jan 22:51:02 2020 No.11270046 View Reply Original Report

Quoted By: >>11270464

I usually post in /mg/ but I know this is a topic /sci/mg loves to fight about so there we go. One topic discussed:
https://en.wikipedia.org/wiki/Limited_principle_of_omniscience
https://ncatlab.org/nlab/show/principle+of+omniscience
Happy new year!

https://youtu.be/RusPpTVyNPw

Anonymous

Anonymous Thu 02 Jan 2020 02:04:15 No.11270432 Report

Quoted By:

bump

Anonymous

Anonymous Thu 02 Jan 2020 02:28:40 No.11270464 Report

Quoted By: >>11271722

>>11270046
Do you have a question about these things, or are you just shitposting?

Anonymous

View Same Google iqdb SauceNAO 1577806739587.png, 100KiB, 394x329

Anonymous Thu 02 Jan 2020 17:37:50 No.11271722 Report

Quoted By: >>11271974

>>11270464
Are type systems with subtyping a bad idea? If so, why?

I think (to have heard) it's convenient for programming but ruins much of the nice type theoretical properties.

I'm however also not sure how many variant of implementation there are of it (the idea that one term is inhabiting a type as well as a subtype of that type)

Anonymous

Anonymous Thu 02 Jan 2020 19:15:59 No.11271974 Report

Quoted By: >>11272048

>>11271722
it's fine, two examples you see it in are
>polymorphism of classes in an OO language
>sets of numbers $\mathbb{N} \subseteq \mathbb{Q} \subseteq \mathbb{R} \subseteq \mathbb{C}$
From the point of view of programming-language design it has obvious advantages, and obvious disadvantages (more work; introduces more undecidable problems w.r.t. extensional subtyping). But if you're asking from the point of view of a type theorist, beats me. Those fuckers are constantly tweaking their theories for publish-or-perish reasons, making it very hard to distinguish what, if any, rules are guiding their design decisions. But again the tradeoff is expressive power versus undecidability.

Anonymous

View Same Google iqdb SauceNAO 465186_1_En_1_Fig3_HTML.gif, 38KiB, 568x322

Anonymous Thu 02 Jan 2020 19:39:26 No.11272048 Report

Quoted By: >>11272058

>>11271974
So you'd answer that it depend on what you want - simple to use object (subtyping) vs. decidability (e.g. of type checking).

In this case, though, it appears clear to me that one should gear things towards the latter and avoid the subtyping - simply because, after so many years, I can't see people actually opting for a functional language that has all the features (from a Javascript person's stand point exotic/magical features). Functional languages won't take over OO languages in their domain in my estimation. There's always gonna be more Kotlin guys than Scala guys. So it's futile to go on an try and get to an easy to learn system.

Okay all that said, I'll have to look into why exactly sub-typing fucks with the things you pointed out so much.
Maybe the secret is somewhere in Martin Odersky's papers, like

https://www.cs.purdue.edu/homes/rompf/papers/amin-wf16.pdf

Anonymous

Anonymous Thu 02 Jan 2020 19:42:36 No.11272058 Report

Quoted By:

>>11272048
>blaming the enviromental circumstances on lab experiences.

Capcode	All Only User Posts Only Moderator Posts Only Admin Posts Only Developer Posts
Show Posts	All Only With Images Only Without Images
Deleted Posts	All Only Deleted Posts Only Non-Deleted Posts
Ghost Posts	All Only Ghost Posts Only Non-Ghost Posts
Post Type	All Only Sticky Threads Only Opening Posts Only Reply Posts
Results	All Grouped By Threads
Order	Latest Posts First Oldest Posts First

Your latest searches