4 ms·

I once tried to take the Taylor series idea further and define the "cosine" of a type as the Taylor expansion of cos(x), but didn't get anywhere with it. Can y

• abecedarius 8y ago
  Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to be 2^x -- that is, x -> Bool -- because it's isomorphic to the characteristic function of a set, and a function type is an exponential (https://bartoszmilewski.com/2015/03/13/function-types/ https://bartoszmilewski.com/2015/03/13/function-types/). But 2^x differs from exp(x) by a constant factor. So I seem to be messing with surface-level analogies without real understanding.
  • etatoby 8y ago
    You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set x = x → Bool Cardinality: 2^x Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be surprised if it was not possible, or if the expansion turned out to have a strange cardinality such as e^x
    • abecedarius 8y ago
      Thanks, I forgot about repetitions of the same element. How could I miss that?