5
$\begingroup$

I have asked a bad question here Why are type theorhetic data structures rarer (than sets) if they are fundamental?

It got closed for being bad but miraculously got re-opened, perhaps because I made it a bit less bad. However, it was still attracting downvotes and so is still a bad question.

I've tried a substantial rewrite but I am actually not sure if I can anything further to make it better?

I think I could make my question clearer if I knew the answer but if I knew the answer I wouldn't have asked.

Since my latest rewrite (or perhaps because of the meta effect) it is again in danger of being closed.

The timeline feature (why is it buried?) is useful here

Any advice on how to rescue it?

Let me try to summarise my thinking about this question in a really dumb way:

  • We have a sets right? They are pretty good data structures*.
  • They come from set theory.
  • Set theory and type theory can both be used in a similar way as the foundation of maths.
  • So sets and types are in a sense interchangable.
  • A lot of programming is already based on types.
  • Why isn't support for "type theory" more popular.
  • Why are programmers (some at least) more likely to think in terms of sets.

My thinking in terms of possible answers is:

  • There are some flaws in my reasoning above - tell me about them
  • There are trade offs making set theory more useful than type theory - tell me about them.
  • Actually type theory is popular
    • Maybe you just see it more in functional programming or academia.
    • If you just searched for this term you'd find hundreds of implementations of bits of type theory in these mainstream languages
  • Type theory is hard
  • There are many competing type theories / systems so its not so easy to describe "type theory" as it is "set theory"

So I sort of know a bit of the answer but would like to hear from the community.

*channelling Graham Chapman

$\endgroup$
8
  • 1
    $\begingroup$ I have read all the revisions and I still don't understand what it's about or especially what kind of answer it's looking for. Perhaps a (new) question with a much smaller scope or a more applied one would help to refine that. The current question does appear to be getting closed now by the same people who reopened it in the first place, which is a bit puzzling, but probably the right outcome. $\endgroup$
    – Michael Homer Mod
    Commented Jun 23, 2023 at 23:02
  • $\begingroup$ I am not able to see who has voted to close on the timeline until the question is actually closed. Do you have that superpower? $\endgroup$
    – Bruce Adams
    Commented Jun 23, 2023 at 23:23
  • $\begingroup$ Why is it called a yo-yo question? I'm a thrower myself, and I'm very confused... $\endgroup$
    – ice1000
    Commented Jun 24, 2023 at 0:16
  • 1
    $\begingroup$ @BruceAdams I looked at the review history, but it's actually only the one overlap so far, I misread the list the first time. The elaboration you've put in here makes the question seem very broad and perhaps uncertain about what exactly "set" and "type" mean in it, so much narrower questions to pin that down might help; it doesn't seem to me like there is a lot of set theory exposed in typical programming languages. Perhaps you'd (dis)like SetBang, which does go hard in that direction. $\endgroup$
    – Michael Homer Mod
    Commented Jun 24, 2023 at 0:27
  • $\begingroup$ @ice1000 its a yo-yo quesiton in the sense it has had up and down votes and been closed and reopened and may well be again. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:32
  • $\begingroup$ Perhaps allow me some leeway in use of set vs set theory and type vs type theory rather than considering it an outright category error. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:35
  • $\begingroup$ A close vote and an upvote in the same breath. My question is divisive apparently. $\endgroup$
    – Bruce Adams
    Commented Jun 25, 2023 at 17:45
  • 1
    $\begingroup$ You could start by correcting the typo in the Title :-) $\endgroup$
    – Ray Butterworth
    Commented Jun 26, 2023 at 0:14

2 Answers 2

Reset to default
2
$\begingroup$

Any advice on how to rescue it?

My general advice is to make sure you understand what you're talking about. I made the same mistakes before, and I fixed them by learning and learning.

For instance, you talked about sets, but there are many different definitions of sets. I used the data structure set definition in my answer, but there are more. For example, in homotopy type theory, sets are types whose 1-paths are propositions. Also, type theory is fundamental in PLs, so your claim on "why isn't support for type theory more popular" is false.

You may also formulate type theory with set theory -- just define a set-theoretic semantics, like in Lean, or think about types as ∞-groupoids, as in HoTT.

$\endgroup$
5
  • $\begingroup$ The problem here is we have users from different kinds of background. Mine is programming and engineering. I don't have sufficient mathematical background knowledge in type theory. Nonetheless my life revolves around types and algorithms and also programming languages and type systems. The latter being why I have been in this site since area 51. Type theory is fundamental to how your mathematical side of the user base think but not so much to the practical side. My question is not bad because I don't know the maths. Actually my question is valid because I want to learn exactly those concepts. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:24
  • 1
    $\begingroup$ @BruceAdams I think you could look at this answer as saying you could ask the precursor questions first to build that knowledge, rather than either not being able to ask any questions (which would be bad), or jumping right to something a bit unspecific like this (which is not going well). $\endgroup$
    – Michael Homer Mod
    Commented Jun 24, 2023 at 0:38
  • $\begingroup$ I'm not sure that makes it a Mu quesiton. An answer explaining where I've gone wrong would be valid. Ice has attempted that but unfortunately with too much PL foundational math for me (at least at this late - for me - hour) $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:43
  • $\begingroup$ @BruceAdams you can ask more questions ;) BTW, I was being extremely restrictive of buzzwords usage. I'm curious about what you found too mathy? $\endgroup$
    – ice1000
    Commented Jun 24, 2023 at 0:50
  • $\begingroup$ Ironically not the maths itself. I was not looking for a mathematic answer. To me, a set as a data structure is more important than as a mathematically entity. The code implements the maths. Type systems are also implemented but as part of the programming language not as data structures manipulated by the programming language for "so called" mainstream languages. E.g C++ vs Haskell. Haskell is of course mainstream but not as popular as C++,Java, Javascript or python. It is also practical. pandoc is a fine example of that. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 1:01
-1
$\begingroup$

I also think you're asking to the wrong audience. I think the users on this website are mainly PL design enthusiasts (aka victims of Wadler's laws), while your question seems to be related to foundations of PL, which is usually only taught in colleges.

It is more likely to be answered on another website such as cs.se, or by learning the foundations of PL yourself. I highly recommend the latter, because that's what I did before.

$\endgroup$
7
  • $\begingroup$ Actually I disagree. One of the strengths of this site is it pulls people in from several sides. Questions asked here often relate to an intent to use something in a new language. The language can be practical or theorhetical (or hobbiest) but there is still much to be learned. Some questions asked here would be shut down on some of the other sites. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:31
  • $\begingroup$ People with PL foundation background are kicked away! Andrej Bauer said his answer to a pros-and-cons question got downvoted because he didn't list any disadvantages. $\endgroup$
    – ice1000
    Commented Jun 24, 2023 at 0:34
  • $\begingroup$ That would be an injustice. Do you have a link to that question and answer? $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:37
  • $\begingroup$ Engineering and Academia should try to be more synergistic! $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:38
  • $\begingroup$ languagedesign.meta.stackexchange.com/q/144/40#comment194_144 $\endgroup$
    – ice1000
    Commented Jun 24, 2023 at 0:43
  • 1
    $\begingroup$ If a questioner deletes the question when they don't like the answer that implicates the questioner not the answerer and not the site. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 0:52
  • $\begingroup$ Also foundations of PL is getting more mainstream with time. Soundness is now a thing to designers of practical PLs not just academic ones for example. We also have more type inference and I expect more things to catch on in the future. $\endgroup$
    – Bruce Adams
    Commented Jun 24, 2023 at 1:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .