zipper 2017-02-01 18:52:05
Anyone know what happened to one called Welkin?
dram_phone 2017-02-01 18:53:39
?let type SzzT = forall s. Control.Monad.ST.ST s
lambdabot 2017-02-01 18:53:41
Defined.
dram_phone 2017-02-01 18:53:53
:t SzzT
lambdabot 2017-02-01 18:53:55
error: Data constructor not in scope: SzzT
dram_phone 2017-02-01 18:53:59
:k SzzT
lambdabot 2017-02-01 18:54:02
* -> *
dram_phone 2017-02-01 18:54:20
Question: Does this make sense? (I think no)
c_wraith 2017-02-01 18:54:41
Sure it makes sense. But it's useless.
c_wraith 2017-02-01 18:55:33
Nearly all of the type signatures involving ST use the s parameter in more than one spot (runST is the only exception I can think of offhand), and that's part of how the safety works
c_wraith 2017-02-01 18:56:03
If you can't explicitly refer to the type variable, you can't ensure it's the same type variable in multiple spots
ski 2017-02-01 18:56:31
zipper : Welkin said something in here, four and a half hour ago
ski 2017-02-01 19:02:12
EvanR : "\"s(n) = s(m) only if n = m\", does the \"only if\" here mean the same thing as \"->\"","and just \"if\" would mean <- ?" -- yes
ski 2017-02-01 19:02:18
Squarism : imho, `$' is harder on the eye
ski 2017-02-01 19:06:16
mniip : an internal language is a language which looks like a lambda-calculus, possibly also including being an element of a subset, set comprehension, a truth-values type, and logical connectives (including quantifiers) for that, which "looks like" it's talking about inhabitants of objects, but which you can translate to the usual pointless language with morphisms, composition, currying, &c.
ski 2017-02-01 19:06:51
mniip : see the McLarty book i mentioned
mniip 2017-02-01 19:07:07
er
mniip 2017-02-01 19:07:14
can I see an example?
ski 2017-02-01 19:11:02
let's say you have `f,x |-> g (\y |-> f (x,y))' with `f : A * B -> C',`x : A',`g : (B -> C) >---> D' and the expression on the right of type `D'
ski 2017-02-01 19:11:30
`g' is some morphism from the exponential object `B -> C' (aka `C^B') to `D'
ski 2017-02-01 19:12:26
`f' is a "name" of a morphism from `A * B' to `C', iow an inhabitant of `A * B -> C'/`C ^ (A * B)'
mniip 2017-02-01 19:13:33
right
ski 2017-02-01 19:13:51
so presumably we should distinguish the application of these two things in the syntax, by perhaps writing `f,x |-> g (\y |-> f $ (x,y))' (which is meant to describe a morphism from `(A * B -> C) * A' to `D', by means of the internal language)
mniip 2017-02-01 19:14:33
what
ski 2017-02-01 19:15:16
the syntax being that if `F' is a morphism from `A' to `B', and `t' a term of type `A', then `F t' is a term of type `B'
ski 2017-02-01 19:15:52
and if `f' is a term of type `A -> B' (not the same thing as just above), and `t' a term of type `A', then `f $ t' is a term of type `B'
ski 2017-02-01 19:16:26
another way to write `f $ t' could be `apply (f,t)', where `apply' is a morphism from `(A -> B) * A' to `B'
mniip 2017-02-01 19:16:50
hmm
mniip 2017-02-01 19:16:58
so we want to generalize the notion of application
mniip 2017-02-01 19:17:13
in functors, NTs and so on?
ski 2017-02-01 19:17:55
unless you bring exponential objects or similar into the picture, category theory is a first-order language
mniip 2017-02-01 19:18:25
in what way
ski 2017-02-01 19:18:34
so applying a morphism to a term is different from getting a term which you "interpret as a morphism, applying it to another term"
ski 2017-02-01 19:19:26
well, given exponential objects, if `f : A * B >---> C' is a morphism, then there is a morphism `curry f : A >---> (B -> C)'
mniip 2017-02-01 19:19:33
no I mean
mniip 2017-02-01 19:19:37
in what way is it a FOL
mniip 2017-02-01 19:19:47
oh
ski 2017-02-01 19:19:48
`>--->' is the morphism arrow. `->' is the construction of an exponential object
mniip 2017-02-01 19:19:50
oh I misread that
mniip 2017-02-01 19:20:02
okay yes
ski 2017-02-01 19:20:21
(and `curry' is not a morphism. it's a construction (an adjunction) that given a morphism, yields a morphism)
mniip 2017-02-01 19:20:53
would it be correct to call it a family of morphisms indexed by morphisms
ski 2017-02-01 19:21:26
anyway, after translation of `f,x |-> g (\y |-> f $ (x,y))', we get `g . curry (f . )', which can be simplified to just `g . curry f' in this case
ski 2017-02-01 19:21:46
hrm, no not quite
mniip 2017-02-01 19:22:44
yes
mniip 2017-02-01 19:23:15
actually you got me lost at
mniip 2017-02-01 19:23:18
1486015862 [09:11:02] let's say you have `f,x |-> g (\y |-> f (x,y))' with `f : A * B -> C',`x : A',`g : (B -> C) >---> D' and the expression on the right of type `D'
mniip 2017-02-01 19:23:25
what are A, B, C, D?
mniip 2017-02-01 19:23:39
categories?
mniip 2017-02-01 19:23:45
is -> the exponential category?
ski 2017-02-01 19:23:56
no, this is in some particular category
ski 2017-02-01 19:24:05
`A',`B',`C',`D' are just any objects in there
mniip 2017-02-01 19:24:21
* is the product and -> is the exponential then?
ski 2017-02-01 19:24:51
`g' is a morphism in that category, and `f,x |-> g (\y |-> f (x,y))' is meant to describe a morphism, in terms of `g', by employing the internal language
ski 2017-02-01 19:24:54
yep
mniip 2017-02-01 19:25:21
hmm
ski 2017-02-01 19:25:46
(the category might be a category of categories, in which case `A',`B',`C',`D' would be categories, and `B -> C' an exponential category, aka a functor category .. but i wasn't assuming that particular special case)
mniip 2017-02-01 19:26:57
okay so
ski 2017-02-01 19:27:06
the definition of exponential basically says that there's a `curry' an an `uncurry' operation, satisfying certain equations. you can use `apply' instead of `uncurry'
mniip 2017-02-01 19:27:14
if f is an exponential
mniip 2017-02-01 19:27:21
then there's the eval morphism
mniip 2017-02-01 19:27:29
which is what we use when we say 'f (x, y)'
ski 2017-02-01 19:27:29
aka `apply'
ski 2017-02-01 19:27:33
yes
mniip 2017-02-01 19:27:34
okay
ski 2017-02-01 19:27:54
(and `f' is an inhabitant of an exponential (object), it's not an exponential object itself)
mniip 2017-02-01 19:28:01
er, yes
ski 2017-02-01 19:28:52
anyway, we get `g . curry (apply . >)', rather
mniip 2017-02-01 19:29:05
so uh, what happens next?
mniip 2017-02-01 19:29:26
what's |-> btw
ski 2017-02-01 19:29:27
if `f : Gamma >---> A' and `g : Gamma >---> B', then ` : Gamma >---> A * B'
ski 2017-02-01 19:29:32
"maps to"
mniip 2017-02-01 19:29:48
can we say that?
ski 2017-02-01 19:30:13
in math, `x |-> ..x..' means more or less the same as `\x. ..x..'
mniip 2017-02-01 19:30:26
is our category nice enough to let us declare existence of an exponential that has the structure that we request?
mniip 2017-02-01 19:30:40
or rather, existence of an element in an exponential
ski 2017-02-01 19:31:36
(i was here using `x |-> ..x..' to describe a morphism mapping an internal point/term `x' to a term `..x..', while using `\x |-> ..x..' for the corresponding (lambda) *term* in the exponential object)
mniip 2017-02-01 19:32:04
do you use the term "term" for the, uh,
mniip 2017-02-01 19:32:11
elements of objects?
ski 2017-02-01 19:32:33
in `... |-> ...', all (term) variables on the right (so not morphism "variables") must be bound on the left
ski 2017-02-01 19:32:57
while in the term `\... |-> ...', not all (term) variables must be bound by the lambda
mniip 2017-02-01 19:33:34
my question is
ski 2017-02-01 19:33:35
mniip : "term" is the syntactic thing, the expression, which here would denote an "inhabitant of an object", yes
mniip 2017-02-01 19:33:44
x |-> x + 1
mniip 2017-02-01 19:33:48
might be a term in Set
mniip 2017-02-01 19:33:57
but not in Vect
mniip 2017-02-01 19:34:28
how can we be sure that a term that corresponds to \y |-> f $ (x,y) exists?
ski 2017-02-01 19:36:13
(i distinguish between "element" and "inhabitant". "element" is in a subset/subobject of a set/type/object. you can ask ("at run-time") whether something is an element. you can't ask whether something is an inhabitant, it's *given* to you as an inhabitant. cf. not being able to ask at run-time whether a variable has a particulartype)
mniip 2017-02-01 19:36:45
right
mniip 2017-02-01 19:37:00
I think I get what you mean
ski 2017-02-01 19:37:10
for `x |-> x + 1', it might describe a *morphism* (the "body" is a term, the whole thing isn't) in `Set', but not in `Vect'
mniip 2017-02-01 19:37:12
elements and sets are a binary relation
ski 2017-02-01 19:37:31
presumably `x + 1' means `plus (x,1)', `plus' a morphism
ski 2017-02-01 19:37:52
`1' might mean `one ()', `one' a morphism
mniip 2017-02-01 19:37:54
no like, I'm talking about an element of the set R->R
ski 2017-02-01 19:38:06
oh, so you meant `\x |-> x + 1'
mniip 2017-02-01 19:38:09
is that not what you use |-> for
ski 2017-02-01 19:39:00
ski 2017-02-01 19:39:15
syntactically, the term formation rules tells us that this is a valid term
mniip 2017-02-01 19:39:22
I'm confused about the backslash/no backslash thing
ski 2017-02-01 19:39:59
semantically, the translation from the internal language to the external language (of ordinary category theory) gives a translation in terms of morphisms
ski 2017-02-01 19:40:37
i use lambda when i'm talking about a term, describing an inhabitant of an exponential object like `A -> B'
mniip 2017-02-01 19:40:50
right
jchia_ 2017-02-01 19:41:34
When I throw an IOError, I can catch it as an IOError using a function that takes an IOError, or as a SomeException using a function that takes a SomeException. But an IOError is not a SomeException. SomeException has a value constructor that can take an IOError (or any class that has an Exception instance), so a SomeException can 'wrap' an IOError but is not an IOError. Is there some language-level magic that allows exception catching to work this way?
ski 2017-02-01 19:41:45
i omit the lambda, when i'm talking about a description of a morphism, from `A -> B', using the internal language to describe it as a "mapping" from inhabitants of `A' to inhabitants of `B', using some more or less complex term in `B', involving variable(s) from `A'
mniip 2017-02-01 19:42:12
jchia_, no, it's just GADTs
ski 2017-02-01 19:43:03
jchia_ : more like library-level magic ..
mniip 2017-02-01 19:43:08
(or at least parts of GADTs like ADTs, datatype contexts, existential quantification, and co)
ski 2017-02-01 19:44:12
ski 2017-02-01 19:44:24
well, consider first the sub-term `f $ (x,y)'
mniip 2017-02-01 19:44:36
how is that a term
jchia_ 2017-02-01 19:44:45
mniip: Which GADT allows this? I want to study the 'magical' code behind this.
mniip 2017-02-01 19:44:59
jchia_, you mean the actual exception catching code?
ski 2017-02-01 19:45:00
if `M' and `N' are terms, then `(M,N)' is a term
