/sci/ - Science & Math

>>8099877
>What does "extensionally identified Haskell functions." mean?
Do you know
https://en.wikipedia.org/wiki/Extensionality

Category theory doesn't know about material equality, just isomosphism. You may import equalities from other theories, and Hask only works for extensionally identified functions:

As computer code, the functions given by
f1(n) := '(x-3)^2'
and
f2(n) := 'x^2-6x+9'
and
f3(n) := '8+x^2-6x+1'
are different. Consider for example a (meta-)property LengthOfCode.
LengthOfCode(f1) = 7
LengthOfCode(f2) = 8
LengthOfCode(f3) = 10

However, they all evaluate to the same values from the same inputs - same extensions.

Equality in predicate calculus comes with the axioms
a=b <=> b=a
and
a=a

When reasoning about strings, you need "5+4" and "2+7" to be different.

But to prove
5+4 = 2+7
you need a theory giving meaning to +. For arithmetic, that's e.g. done in pic related
(where 1 is taken to be S(0), and 2 is taken to be S(1), and 3 is taken to be S(2), and so on.

>How should I think about polymorphism?
Read
https://en.wikipedia.org/wiki/Parametric_polymorphism
?
Your background?

Consider the following function:
id_on_Int : Int -> Int
id_on_Int(n) := n
e.g. id_on_Int(3) evaluates to 3.

Now tell me an analog function of type
String -> String
Of course,
id_on_String(s) := s
does the job.

Generally, in Haskell you'd write a generic function
id : forall a. a -> a
id(x) := x
and when you pass 3 to id, the compiler/the compiled program does type inference on 3 and converts id : forall a. a -> a to a function Int->Int and keeps working with that. (google Hindley–Milner)

Consider the following function:
i2s : Int -> String
i2s(n) := ...write down the number as a word

e.g. i2s(3) evaluates to "three".

Keep this function of type
Int -> String
in mind, and tell me an analog function of type
Int -> a
where a is a generic type.
You can't, really.

Another generic function would be the one which takes a pair (x,y) and returns (y,x).