all 50 comments

[–]dalaing 11 points12 points  (19 children)

I have a tangentially related question: is there a principled way to reason about the number of inhabitants of a polymorphic function?

The simplest examples I can think of are

f :: forall a. a -> a -> a


g :: forall a. a -> a -> a -> -> a

which have 2 and 3 inhabitants respectively.

A more complicated example is

 h :: forall a b c. (b -> b -> c) -> (a -> b) -> (a -> a -> c)

(with thanks to Tony Morris - this is from his workshop at the Brisbane Lambda Jam)

The nearest I've been able to figure is that for each universal there's a sort of abstract dimension that gets introduced, and that n parameters of the same type in the negative positions are treated like nth complex roots of unity.

There's something puzzling and kind of compelling about all of this, and I'd really like to understand it better. Is this something that is well understood? Does anyone have any pointers on where I could find out more?

[–]pcapriotti 18 points19 points  (9 children)

The Yoneda lemma is your friend here:

(∀ x . (a → x) → f x) = f a

for any (covariant) functor f.

In particular, for your simple examples:

  ∀ a . a → a → a
= ∀ a . a × a → a
= ∀ a . (2 → a) → a
= 2

where the last step is just an application of Yoneda.

The more complicated example is also quite easily tackled:

  ∀ a b c . (b → b → c) → (a → b) → (a → a → c)
= ∀ a b c . (b × b → c) → (a → b) → (a → a → c)
= ∀ a b . (a → b) → (a → a → b × b)
= ∀ a . (a → a → a × a)
= ∀ a . (2 → a) → a × a
= 2 × 2
= 4

where we used Yoneda three times, once for every type variable.

[–]dalaing 8 points9 points  (0 children)

That is pure awesome - thank you so much.

[–]rpglover64 3 points4 points  (3 children)

I think it would be helpful if you instantiated the f for each application of yoneda; I can't quite follow the more complicated steps.

[–]pcapriotti 7 points8 points  (2 children)

Sure. Here's a more detailed calculation. The variable names u and f refer to this formulation of Yoneda:

    (∀ x . (u → x) → f x) = f u


{ uncurry first argument }


{ Yoneda with:
    u := b × b
    f x := (a → b) → (a → a → x) }


{ Yoneda with:
    u := b
    f x := (a → a → x × x) }


{ uncurry }

= ∀ a . (a × a → a × a)

{ universal property of coproduct 1 + 1 }


{ Yoneda with:
    u := 2
    f x := x × x }

= 2 × 2

{ arithmetic on finite types }

= 4

[–]rpglover64 1 point2 points  (0 children)


[–]pcapriotti 0 points1 point  (0 children)

Thanks for the gold!

[–]want_to_want 1 point2 points  (1 child)

This is beautiful, thank you! Do you know if counting the inhabitants of an arbitrary polymorphic type is a decidable problem?

[–]pcapriotti 1 point2 points  (0 children)

I'm not sure, actually. Note that you can get all recursive types this way, so if indeed there is an effective counting procedure, it is quite powerful.

Some other people here might know more about this.


This assumes parametricity, doesn't it?

[–]pcapriotti 0 points1 point  (0 children)


[–]dmwit 4 points5 points  (2 children)

I'm not 100% sure it has the answer you're looking for, but you may want to look into the literature on parametricity, which is a key property in your claim. For example, in Java, it's not totally clear that there are only two inhabitants of forall a. a -> a -> a: one could, for example, use introspection to check whether a is Int and then behave as (+), and behave as const otherwise, which is a very different behavior than the two you probably had in mind.

I'm not totally sure whether anybody has studied the connection between enumeration and parametricity.

Now that I say the word "enumeration", it occurs to me that this sounds very similar to stuff Brent Yorgey has been studying connecting insights from combinatorics to more familiar programming languages concepts. So you might look into some of his papers, too; e.g. "Species and functors and types, oh my!" is probably a good starting point.

But no promises that you find something specifically solving the problem you ask. If you don't find a paper... perhaps you could write something up yourself and publish it. ;-)

[–]dalaing 0 points1 point  (0 children)

There's some good work linked from here as well.

I had the feeling that either something by Conor McBride or by Brent Yorgey would have some answers. I guess I should keep clicking and reading.

I'm not sure I'll look too far beyond those materials though - if there turns out to be a topological interpretation I'm not sure I'm adequately prepared to dive in :)

[–][deleted]  (5 children)


    [–]dalaing 1 point2 points  (4 children)

    That doesn't seem to be true though, since


    has 2 inhabitants, regardless of what a is.

    The inhabitants are f x _ = x and f _ y = y (or at least, it has 2 inhabitants which are functions that terminate)

    My understanding is that the forall a effectively means "regardless of what a is".

    I don't think you can get 16 different version of f just by using it with Bool, for instance.

    [–]bss03 1 point2 points  (1 child)

    regardless of what a is.



    Bool -> Bool -> Bool most definitely has 16 instances in a total language:

    f0000 _ _ = False
    f0001 x y = x && y
    f0010 x y = x > y
    f0011 x _ = x
    f0100 x y = x < y
    f0101 _ y = y
    f0110 x y = x /= y
    f0111 x y = x || y
    f1000 x y = not $ f0111 x y
    f1001 x y = x == y
    f1010 _ y = not y
    f1011 x y = x >= y
    f1100 x _ = not x
    f1101 x y = x <= y
    f1110 x y = not $ f0001 x y
    f1111 _ _ = True

    It has several (at least 8) more in Haskell.

    [–]dalaing 1 point2 points  (0 children)

    What I meant was, that if you have a function with signature f :: forall a. a -> a -> a it has 2 inhabitants, and it doesn't matter if you use f True False later in your program.

    I should have been more precise in my use of "using it with" :)

    [–]tel[S] 0 points1 point  (0 children)

    bss03 explained this thoroughly, but it's better to think of f as being the function which which operates without knowledge of a. Thus we can say something more like "f {A} has two instantiations without taking advantage of knowledge of A" where {.} is System-F type application.

    [–]tel[S] 4 points5 points  (7 children)

    Hi /r/haskell!

    Here's another post I've written. My goal is to go through basic data types comprehensively in a format inspired a bit by Per Martin-Löf's "On the meanings of the logical constants and the justifications of the logical laws". I feel it struggles a bit with trying to be universal while using Haskell syntax as a way of representing the various types and values.

    So, constructive criticism is greatly appreciated!

    Also I'm probably interested in writing another article later which tries to introduce Mu and Nu so that I can show how this arsenal leads to much more obviously interesting data types.

    [–]dalaing 3 points4 points  (1 child)

    This is a very minor point / question - would it be helpful to add something to the second paragraph about the fact that 1 and 0 will be used as notation, but not in the sense of binary digits?

    As it stands, the post claims ones and zeroes are outside of the context, introduces 1 and 0 as notation, and then it becomes clear why that's fine. A forward reference / reassurance that it'll all work out might smooth that over.

    [–]tel[S] 1 point2 points  (0 children)

    Oh! Thanks for pointing that out. I was blind to the fact that it could be misinterpreted... knowing where I was going.

    [–]redxaxder 3 points4 points  (3 children)

    I noticed that with just the primitives provided (1, 0, +, x, ->), I can only construct a type with finitely many inhabitants. What do we need to add to reach outside the land of the finite?

    I looked up the definitions of Mu and Nu...

    data Nu f = forall a . Nu a (a->f a),

    but I can't shake the feeling that there's an easier way to make it happen.

    [–]tel[S] 4 points5 points  (2 children)

    Mu and Nu are exactly the way you do it, but their types are a little weird. A slightly easier one to grasp is called Fix


    Fix operates over a "signature" functor, f. So we want to think about how data types and signature functors relate. Here's List

    data List  a   = Nil  | Cons  a (List a)
    data Listf a x = Nilf | Consf a x

    so basically you replace recursive self-references to the type with a new type variable. Now, a zero-element list is the type

    Listf a Void

    since the only constructor you can use is Nil. A one-or-fewer-element list is

    Listf a (Listf a Void)

    since you can use Nil and Cons. A two-or-fewer element list is

    Listf a (Listf a (Listf a Void))            -- 2 or fewer
    Listf a (Listf a (Listf a (Listf a Void)))  -- 3 or fewer ...

    Clearly to get the lists we know and love we'd like to just plug an infinite number of layers of Listf together. And that's exactly what Fix (Listf a) is

    Fix (Listf a) ~ Listf a (Fix (Listf a)) 
                  ~ Listf a (Listf a (Fix (Listf a)))

    And we can eventually show that these three are all equal:

    List a
    Fix (Listf a)
    Mu (Listf a)
    Nu (Listf a)

    though the latter two are a little more difficult to grasp.

    [–]bss03 4 points5 points  (1 child)

    And we can eventually show that these three are all equal:

    List a
    Fix (Listf a)
    Mu (Listf a)
    Nu (Listf a)

    Depends on what you mean by equal. They are all isomorphic in Haskell, ignoring bottom. Pretty sure if Hask wasn't a CCC, Mu and Nu need not even be isomorphic. mumble mumble colimits and limits, initial and final mumble mumble expression problem.

    [–]tel[S] 4 points5 points  (0 children)

    Yep, they're hand-grenade "equal".

    [–]sufianrhazi 1 point2 points  (0 children)

    I have thoroughly enjoyed this as well as your previous posts. Keep it up!

    [–]danbst 5 points6 points  (4 children)

    a use of a + b is (a -> r) * (b -> r)

    that said, it is like equality

    r^(a+b) == r^a * r^b

    which is quite obvious. But the other one

    a use of a * b is (a -> r) + (b -> r)

    seems to be wrong in arithmetics:

    r^(a*b) == r^a + r^b

    [–]tel[S] 5 points6 points  (2 children)

    Yeah, there's something really subtle here mentioned in one of the footnotes: if you have a product (a, b) then you ought to be able to eliminate that product by using both a and b together. In other words, you ought to be able to produce a dependent goal by consuming a first and then b. Which is just the adjunction:

    (a, b) -> r    ==    a -> (b -> r)

    This also gives you your algebra

    r^(a*b) == (r^b)^a == (r^a)^b

    I really wish I knew how to better talk about this distinction—I find my current approach lacking. I find mentioning duality really important, but I don't want to bring in a lot of mechanics.

    (Edit: I edited the post to try to be a little less bombastic and leave more room for this issue. I also edited the footnote to directly mention the adjunction)

    [–]pcapriotti 2 points3 points  (1 child)

    I'm not sure what you're saying here. The post seems to state that

    (a,b) -> r == (a -> r) + (b -> r)

    which is of course not true.

    The duality between sums and products works another way: one is a colimit and the other a limit. The universal property of the limit gives you:

    s -> (a,b) == (s -> a, s -> b)

    which I believe is the correct dual of

    (a + b) -> r == (a -> r, b -> r)


    Yes, I think I pushed it too far. In particular, I wanted to invoke the duality you see in the presentation of sums in natural deduction format, but I was overly hasty to present it as a function. I should really just rewrite that section.

    [–]godofpumpkins 1 point2 points  (0 children)

    It's wrong in types too

    [–]benjaminpd 5 points6 points  (1 child)

    One branch of logic, intuitionistic logic, tries to cope without the ability to prove without construction. Thus, in intuitionistic logic the structure of data is better preserved… but one must also do without ex falso quodlibet which can be painful.

    Inituitionistic logic is fine with ex falso quadlibet. You must mean the law of the excluded middle (tertium non datur, if we're sticking to latin).

    Nice piece otherwise!

    [–]tel[S] 2 points3 points  (0 children)

    Yep, it was a slight brain-o on rewriting that section. I've rectified it now. Thanks for the notice!

    [–]deltaSquee 2 points3 points  (3 children)

    Is it possible to define a manifold of types? It seems like it should be.

    [–]maxaroni 1 point2 points  (2 children)

    [–]autowikibot 0 points1 point  (0 children)

    Homotopy type theory:

    In mathematical logic and computer science, homotopy type theory (HoTT) attempts to give an account of the semantics of intensional type theory using the framework of (abstract) homotopy theory, in particular Quillen model categories and weak factorization systems. Conversely, intensional type theory forms a logic (internal language) for homotopy theory.

    Interesting: Type theory | Intuitionistic type theory | Univalence axiom | Set theory


    [–]deltaSquee 0 points1 point  (0 children)

    I meant more like a Banach space of the generating functions of types.

    [–]jberryman 2 points3 points  (1 child)

    I've found having an awareness of the algebra of types, even if I don't have a deep understanding, to be really helpful for designing libraries; much more so than trying to take cues from category theory.


    You know, I feel the same way, though I didn't realize it until I read your comment.


    We can even construct the left value of type Unit + Void using Inl but not the right using Inr since it would demand we produce a value of type Void which is impossible.

    So "Inl T :: Unit + Void" is fine but "Inr T :: Void + Unit" isn't? I don't understand this.

    edit: Does it have to do with the partial application of type contructors?

    [–]radomaj 1 point2 points  (1 child)

    It confused me too. I think the author still meant Unit + Void and you will surely agree there's no possible way to do Inr, since that would require Inr Void and you can't do Void.


    you will surely agree


    [–]tel[S] 0 points1 point  (2 children)

    I've slightly clarified the wording. Do you think it helped?


    we cannot produce the right-side value right using Inr

    Is that bold 'right' not superfluous or does it mean 'correctly' in this context?

    Anyway, I guess you mean you can't get 'it :: Unit + Void' using Inr (b/c no value of type Void)? But you could get 'it :: Void + Unit' using Inr T?


    Superfluous. And that's exactly correct :)

    [–]xanados 0 points1 point  (3 children)

    I don't really understand this line:

    Products are constructed from values of both their left type and their right type together and used when there is a use for either values of their left type or their right type.

    Is this getting at the fact that both a and b are always defined, so if you always need to have the choice of which to use, you have to use a product type? If that's the intuition, then I don't think "either" and "both" have the right meaning to convey that. It seems like "choice" might offer a better intuition than "use"?

    Later, in the section that is supposed to clarify this issue, you say a "use" of a is a function a -> r. So a "use" of a * b is a function a * b -> r. How then does that imply that a use of a * b -> r is equivalent to (a -> r) + (b -> r)? For example, if a is integers, and b is imaginary integers, and r is complex numbers, are you saying that the function a * b -> r can be represented as either a function that just takes the integer and returns a complex number or the function that takes an imaginary integer and returns a complex number? That doesn't seem to make any sense. Or perhaps I'm misreading the section and a * b -> r is not a use of a * b, and it only counts as a use if it is a * b -> (a -> r) + (b -> r), but there doesn't seem to be any explanation for why that would be the case. I suppose it is intended that this is captured by footnote 4, but that doesn't really clarify it in my mind. If a can take on 10 values, and b can take on 10 values, why can I only get 20 values out of a use of it (a -> r) + (b -> r) rather than 100 values?


    I'm stating something weak but spoke about it strongly and I've rectified the wording now to try to be a bit more clear. Invoking a bit more Haskell, I'm trying to talk about the following function

    zap :: (a, b) -> Either (a -> r) (b -> r) -> r
    zap (a, _) (Left f)  = f a
    zap (_, b) (Right g) = g b

    which indicates that a sum can be a use of a pair. Unfortunately, I spoke as though its the only use, but obviously that isn't true since we have things like uncurry (+). Really, the way to talk about it would be to invoke curry

    curry :: ((a, b) -> r) -> (a -> (b -> r))

    which indicates that we could choose to use the two sides sequentially. This is more general than zap since we have

    embed :: Either (a -> r) (b -> r) -> (a -> (b -> r))
    embed (Left f)  a _ = f a
    embed (Right g) _ b = g b

    but talking about curry would have been a longer sidenote than I felt worth tolerating. Hopefully, with this softening of wording there's a better compromise.

    [–]radomaj 0 points1 point  (1 child)

    I'm pretty sure the author screwed up and went too far with the dualities and generalizations. Okay, maybe not screwed up, but went with the minimal requirements for implementing a function (in that, when you have a tuple (a,b) you could use just a or just b, but forgot to mention that you could, as you point out, use both).

    So really, a * b -> r would be equal to, uhhh, (a -> r) + (b -> r) + ((a*b) -> r) which sounds a little bit redundant, recursive and silly. I believe there is a way to not use * on both sides, but it hasn't come to me yet.

    EDIT: Cf. this post above: http://www.reddit.com/r/haskell/comments/2bj7it/let_me_tell_you_about_the_types_of_data/cj6cgga


    I did screw up and indicated a tightness that isn't true. The other tight equality would be a * b -> r == a -> (b -> r). I'm going to back through and be more accurate indicating that you can use a pair by having a sum of uses instead of must.

    The thing I was really getting at comes from natural deduction where there are two rules for eliminating a product and two rules for introducing a sum

    a x b    a x b      a       b
      a        b      a + b   a + b

    but trying to describe this with functions swept actual details under the rug and lead to inaccuracies. In particular, while you can translate those bars into a function they are not the only things of that shape which can be translated into a function. For instance

        a x b
    -------------  contract/duplicate
    a x b   a x b
    -----   -----  use left | use right
      a       b
    -------------  construct product
        a x b

    uses contraction to show how we are able to use a x b twice.

    [–]cameleon 0 points1 point  (1 child)

    Regarding constructing anything from Void, you mention:

    In something like Haskell we have to resort to trickery, however, either using a “justifiable error” or an infinite loop

    But there is a nice way of defining Void (which I think I was first told about by Conor McBride) that nicely sidesteps this problem:

    newtype Void = Void { magic :: forall a. a }

    Now if you get passed a value of type Void, to construct any a, you can just use magic! For example, your Show instance can be written as:

    instance Show Void where show = magic

    Now you don't have to call error yourself or loop endlessly, but instead you let the liar pass you his lie, and use it against him.

    (I'm a bit late to the party, but somebody might still find this useful)


    Oh, that's true. And great. I'm going to add a note! Thanks!