From: crossd at gmail.com (Dan Cross)
Subject: [COFF] [TUHS] History of popularity of C
Date: Mon, 8 Jun 2020 08:47:03 -0400 [thread overview]
Message-ID: <CAEoi9W5ejTY6JmWRAfy2mL8vbwOVwgxdjTUS0YLqytcVRsu52g@mail.gmail.com> (raw)
In-Reply-To: <CAAYAaAPu=dKnXH82WmECenLNJKSnKNh6aqjFphOoc+NPWxuGhw@mail.gmail.com>
[-TUHS, +COFF as per wkt's request]
On Sun, Jun 7, 2020 at 8:26 PM Bram Wyllie <bramwyllie at gmail.com> wrote:
> Dependent types aren't needed for sum types though, which is what you'd
> normally use for an array that carries its size, correct?
>
No, I don't think so. I've never heard of the dimensionality of an array in
such a context described in terms of a sum type, but have often heard of it
described in terms of a dependent type. However, I'm no type theorist.
- Dan C.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://minnie.tuhs.org/pipermail/coff/attachments/20200608/3d372e09/attachment.htm>
next parent reply other threads:[~2020-06-08 12:47 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
[not found] <CAEoi9W4FDH7ahPHNfEdA0kcMO-yQccF-r=hUCNANyKWMtoO3bA@mail.gmail.com>
[not found] ` <202006072256.057Muo1h090326@elf.torek.net>
[not found] ` <CAAYAaAPu=dKnXH82WmECenLNJKSnKNh6aqjFphOoc+NPWxuGhw@mail.gmail.com>
2020-06-08 12:47 ` crossd [this message]
[not found] ` <a1321feb-ff2c-4172-9a43-cac2f61bfc18@CHERUBFISH.conted.ox.ac.uk>
2020-06-08 13:46 ` cezar.ionescu
[not found] <202006072115.057LFV6v089953@elf.torek.net>
[not found] ` <7w4krmw1kc.fsf@junk.nocrew.org>
2020-06-08 12:51 ` crossd
2020-06-08 14:14 ` akosela
2020-06-08 15:22 ` crossd
2020-06-08 15:38 ` clemc
[not found] <CAEuQd1B8gH-Lu22HKj9pn6JVXNVVYscAnL4TSVDY03k2ORy2qw@mail.gmail.com>
[not found] ` <8a2e9b1b-8890-a783-5b53-c8480c070f2e@telegraphics.com.au>
[not found] ` <m1jcHQv-0036tPC@more.local>
[not found] ` <CAC20D2NhWp8V88+7KFaRdYPtn=YrJBfWxUu9OM4bOu8Fp_7KEA@mail.gmail.com>
[not found] ` <alpine.BSF.2.21.9999.2005261411560.79423@aneurin.horsfall.org>
[not found] ` <9e5933a166ece32b4fb17c6bbb563873@firemail.de>
[not found] ` <CAFNqd5Vrk9RBdq1MqyGGAAVZaaEWNE19sAaX4AkNudEfYD+Btg@mail.gmail.com>
2020-05-26 19:55 ` crossd
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAEoi9W5ejTY6JmWRAfy2mL8vbwOVwgxdjTUS0YLqytcVRsu52g@mail.gmail.com \
--to=coff@minnie.tuhs.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).