Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: Do we need dependant types?

Tim Hosgood (Jul 07 2020 at 12:03):

There’s the paper Do we Need Dependant Types by Daniel Fridlender and Mia Indrika which gives a neat “trick” for constructing something that looks like a dependent type, but without actually using dependant types. Is this an example of a more general method? I’m guessing that this can be used to construct types dependent on $\mathbb{N}$ in lots of situations, but I have no idea what’s really going on behind the scenes here!

Matteo Capucci (he/him) (Jul 11 2020 at 11:52):

(For reference, this is the paper https://pdfs.semanticscholar.org/7e66/7dd0515e4f674e42c0b0860644fee3dd5846.pdf)

Matteo Capucci (he/him) (Jul 11 2020 at 11:55):

Maybe you can generalize that to Turing categories, in which you have a form of self-encoding resembling Godelization

Matteo Capucci (he/him) (Jul 11 2020 at 11:55):

But I don't know. Plus, what the purpose? Circumventing Haskell's limitations? (honest question)

Dan Doel (Jul 11 2020 at 15:11):

Most of the machinery in that paper is a special case of what is now called Applicative in Haskell. Their (<<) is written (<*>) :: Applicative f => f (a -> b) -> f a -> f b. repeat is a special case of pure :: Applicative f => a -> f a. You can generalize their functions to work for any Applicative that way, and their example is obtained by using ZipList.

Dan Doel (Jul 11 2020 at 15:16):

And of course it's well known that instead of trying to do some dependently typed lift n you can just write f <$> x <*> y <*> z, where (<$>) :: Functor f => (a -> b) -> f a -> f b, which isn't really that bad, and so this isn't a very good example of why dependent types are worth while. :slight_smile:

Dan Doel (Jul 11 2020 at 15:40):

The rest is kind of messing with continuation passing and polymorphic types to get something that looks like numerals, but actually has a complex type. I think another example is the printf DSL that Oleg Kiselyov came up with.