quchen 2017-03-08 20:50:33
Meta question. When I say »data Nat where Zero :: Nat; Succ :: Nat -> Nat«, how would I argue that Succ is already defined here, and not merely a statement of Succ's type that has a value yet to be given (such as \_ -> 1)?
quchen 2017-03-08 20:50:50
In other words, where does the »uniqueness« of Succ come from?
quchen 2017-03-08 20:51:25
In a Haskell context this is clear (because well, Haskell works this way). But in type theory there is the same notation without the Haskell Report to fall back to.
`Guest03 2017-03-08 20:51:58
i don't quite understand this
`Guest03 2017-03-08 20:52:42
neither first part nor restatement
quchen 2017-03-08 20:52:52
If you give a mathematician »succ : ℕ -> ℕ«, then succ could be any function from ℕ to ℕ.
quchen 2017-03-08 20:53:31
But when we have a functional language (Haskell, Agda), the »succ« in a data definition gives us a unique way to go from one Nat to another.
quchen 2017-03-08 20:54:07
It's not any general function from ℕ to ℕ, it's »the successor function«. I'm wondering where that comes from.
`Guest03 2017-03-08 20:54:13
the succ gives an unique way because it is unique
`Guest03 2017-03-08 20:54:20
if you had Succ1, Succ2
`Guest03 2017-03-08 20:54:29
would no longer be unique
quchen 2017-03-08 20:54:32
Why is it unique? I can think of many other functions of type ℕ → ℕ.
`Guest03 2017-03-08 20:55:47
is your question "why does Succ denote the successor function instead of anything else?"?
quchen 2017-03-08 20:55:59
Yes, sounds right
quchen 2017-03-08 20:56:54
Is it maybe given not by the data definition alone, but also by the accompanying destructor (i.e. that you can pattern match on it), and the two are mutually inverse?
`Guest03 2017-03-08 20:57:12
i think we should distinguish the constructor and the function
barrucadu 2017-03-08 20:57:32
I think the fact that you can pattern match on the Succ is key
`Guest03 2017-03-08 20:57:33
defining the constructor (the element in the list of constructors) gives rise to a function
dmwit_ 2017-03-08 20:58:54
quchen: you know about lfp def. of inductive types?
quchen 2017-03-08 20:59:00
LFP?
ClaudiusMaximus 2017-03-08 20:59:02
makes me think of https://en.wikipedia.org/wiki/Free_group#Examples and https://en.wikipedia.org/wiki/Word_%28group_theory%29
dmwit 2017-03-08 20:59:12
least fixed point
quchen 2017-03-08 20:59:23
dmwit: No, I don't
dmwit 2017-03-08 20:59:28
okay
dmwit 2017-03-08 20:59:37
take any set
`Guest03 2017-03-08 20:59:45
the notion "any functions N -> N" is meaningless before we define the set of constructors for N
`Guest03 2017-03-08 21:00:18
it's a weird question
dmwit 2017-03-08 21:18:21
so we start from the inductive def. and go from there
SexHendrix 2017-03-08 21:18:27
i did have another magic' function that put it in [(Int, Int)]
SexHendrix 2017-03-08 21:18:39
but by then i already wanted to pull my eyeballs out
dmwit 2017-03-08 21:18:53
that is: zero is a nat, and if n is a nat, then succ(n) is a nat
quchen 2017-03-08 21:19:28
Sure, but that holds even if succ(n) ≡ 0.
dmwit 2017-03-08 21:19:39
this is simultaneously a def. of nat, succ, and zero
dmwit 2017-03-08 21:20:02
no, succ isn't just any old function
quchen 2017-03-08 21:20:23
Ah right, the (n,1) tuple example you gave.
dmwit 2017-03-08 21:20:56
implicit in my sentenge i guess is that succ is injective and not the identity
quchen 2017-03-08 21:21:06
dmwit: Hm. I guess »a type« is not simply the type, but the tuple (formation, constructors, elimination), and not merely the »ℕ«. So »the natural numbers« is (ℕ, {0, succ}, recurse) rather than just »the thing made with 0 and succ«
dmwit 2017-03-08 21:21:34
a similar implicit applies to other inductive def.s of course
dmwit 2017-03-08 21:22:03
quchen: absolutely agree
quchen 2017-03-08 21:22:36
so Tuple = (a -> b -> Set, a -> b -> Tuple a b, \f (Tuple a b) -> f a b)
quchen 2017-03-08 21:23:01
In the tuple case this makes much more sense, since we would never talk about »the tuple« the way we would talk about »the nats«
quchen 2017-03-08 21:23:35
So it's harder to mistake »(,)« for »tuple«, compared to mistaking »0, succ« for »ℕ«
osa1 2017-03-08 21:29:14
is there a shorthand of `if this prism matches run this monad action otherwise return ()` in lens?
ski 2017-03-08 21:29:21
implicit in dmwit's sentence is that `nat' is defined in the least restrictive way, in order to support `zero' and `succ'. since `succ(n) = zero' doesn't need to hold if `zero' is an element and `succ' and endo-function, that means it doesn't hold, with `nat' being inductively defined like this
ski 2017-03-08 21:29:31
quchen : injectiveness follows from this
dmwit 2017-03-08 21:29:37
osa1: traverse does that
osa1 2017-03-08 21:29:37
similar to `case x of C1 (C2 (C3 x y z))) -> f x y z; _ -> return ()`
dmwit 2017-03-08 21:29:51
:t traverse_
lambdabot 2017-03-08 21:29:53
(Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
dmwit 2017-03-08 21:31:10
:t traverse_ :: Applicative f => (a -> f b) -> Maybe a -> f ()
lambdabot 2017-03-08 21:31:12
Applicative f => (a -> f b) -> Maybe a -> f ()
osa1 2017-03-08 21:31:22
OK
osa1 2017-03-08 21:32:11
thanks dmwit jle`
ski 2017-03-08 21:32:24
quchen : you can formalize it as the initial object in a specific category
jle` 2017-03-08 21:32:40
:t traverseOf_ _Just
lambdabot 2017-03-08 21:32:43
Applicative f => (b -> f r) -> Maybe b -> f ()
jle` 2017-03-08 21:32:53
:t traverseOf_ hex
lambdabot 2017-03-08 21:32:55
(Applicative f, Integral a) => (a -> f r) -> String -> f ()
dmwit 2017-03-08 21:34:33
i'm going to hand off to ski and get some sleep. enjoy
quchen 2017-03-08 21:35:13
dmwit: Thanks a lot for your explanations!
ski 2017-03-08 21:35:13
quchen : in this case, the objects of the category are triples `(X,z,s)', with `X' being a set, `z : 1 >---> X' and `s : X >---> X'. and a morphism `m : (X_0,z_0,s_0) >---> (X_1,z_1,s_1)' is a function `m : X_0 >---> X_1' such that `m . z_0 = z_1' and `m . s_0 = s_1 . m'
quchen 2017-03-08 21:35:13
dmwit: The obvious »constructors are injective« is invaluable for my understanding
quchen 2017-03-08 21:35:40
Not that I didn't know that, but I didn't *know* it ;-)
ski 2017-03-08 21:36:16
.. if you prefer, you could take `X' as being an object in an arbitrary "base" category `C', and then `m : X_0 >---> X_1' is a morphism in that category `C'
ski 2017-03-08 21:36:40
in the former case, the initial object in this new category is `(|N,zero,succ)', the natural numbers. the initiality of this object gives you fold (catamorphism)
quchen 2017-03-08 21:36:55
Categories unfortunately make things much less clear for me, usually. :-(
ski 2017-03-08 21:36:57
in the latter case, you call it "a natural numbers object in `C'"
ski 2017-03-08 21:39:21
quchen : anyway, apart from "constructors are injective", you also get "constructors are disjoint", and also that if you build a function `\x -> ..x..', `..x..' being an expression built by using `x' and the constructors, then this function is the identity only if the expression is `x' itself
ski 2017-03-08 21:39:56
the latter means there is no `n' with `n = succ(n)', e.g.
quchen 2017-03-08 21:40:14
I see, so you get a lot of mileage out of that definition then.
quchen 2017-03-08 21:41:39
But leaving away the higher math, one could say that constructors are injective, not the identity, and disjoint.
quchen 2017-03-08 21:42:01
The »has no fixed point« property is a speciality of the ℕ successor.
ski 2017-03-08 21:42:30
in a more general setting, one'd have both constructors/generators, and given *equations*/relations/laws between them (cf. generating e.g. a group from a set of generators, and a set of "relations" between them)
ski 2017-03-08 21:44:33
(so in this case the "constructors" are not disjoint, due to the presence of the laws)
quchen 2017-03-08 21:45:19
Not disjoint in the sense that 0 is possibly both a »s« and a »p«?
ski 2017-03-08 21:46:21
yes
`Guest03 2017-03-08 21:46:37
how to define infinite graphs?
jle` 2017-03-08 21:47:12
it depends on your graph type
`Guest03 2017-03-08 21:47:38
uh
`Guest03 2017-03-08 21:47:41
just graph?
`Guest03 2017-03-08 21:47:45
undirected
ski 2017-03-08 21:47:51
quchen : this latter would be an example of an archic algebra (iow having, or being subject to, laws). the former (the peano natural numbers) being an anarchic algebra (no laws)
quchen 2017-03-08 22:03:42
ski: That is, »yes, but part of what you said was redundant«?
ski 2017-03-08 22:03:51
the eliminator is the initial object morphism `elim z f : (ℕ,0,S) >---> (C,z,f)'
mbrock 2017-03-08 22:03:59
with lenses foo and bar, when I do "let x = foo . bar" that seems to overspecify x's type in a way that prevents me from doing both "x . baz" and "x . qux" when baz and qux have different target types...
ski 2017-03-08 22:04:34
quchen : .. rather, an alternate way to understand it, in terms of initial algebras
mbrock 2017-03-08 22:04:42
it's always confusing to me when introducing a let binding for a common expression messes with type inference
`Guest03 2017-03-08 22:04:47
i don't know whether my question is related to graph's underlying data structure
`Guest03 2017-03-08 22:05:23
or to a "way of defining" for a particlar graph
ski 2017-03-08 22:05:31
mbrock : DMR ?
mbrock 2017-03-08 22:06:03
I do actually have the NoMonomorphismRestriction language feature on
`Guest03 2017-03-08 22:07:36
initially it is about latter, but those two layers seem to be interwoven
ski 2017-03-08 22:34:59
`Guest03 : the type of the recursive use of `length' isn't the same as the type of the current call to `length'
