Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 442 443 444 445 446 447 448 449 450 451 452 .. 5022
— 502,152 events total
2020-10-05 20:29:13 <ski> (if you prefer writing right-to-left, then flip the order)
2020-10-05 20:29:25 → GuillaumeChrel[m joins (guillaumec@gateway/shell/matrix.org/x-kyytvilbqkccelxo)
2020-10-05 20:30:02 <ski> now consider finite prefices of the natural numbers. a type `Fin n', having the natural numbers (strictly) less than `n' as inhabitants
2020-10-05 20:30:08 → Ericson2314 joins (ericson231@gateway/shell/matrix.org/x-tddshmiwufwouryw)
2020-10-05 20:32:31 <ski> it's natural to want to define two inclusions. if `i : Fin m', then `injl i : Fin (m + n)'. and if `j : Fin n', then `injr j : Fin (m + n)'
2020-10-05 20:32:36 → Amras joins (~Amras@unaffiliated/amras0000)
2020-10-05 20:33:11 → snakemasterflex joins (~snakemast@213.100.206.23)
2020-10-05 20:33:25 × knupfer quits (~Thunderbi@200116b82cef8300c06758e924f2c41e.dip.versatel-1u1.de) (Ping timeout: 240 seconds)
2020-10-05 20:34:02 <tomsmeding> which is fortunately nicely symmetric
2020-10-05 20:34:03 × machinedgod quits (~machinedg@142.169.78.196) (Ping timeout: 260 seconds)
2020-10-05 20:34:29 <ski> let's say we picked the version of `+' that does recursion on the left operand. then we'd have `injl Z = Z; injl (S i) = S (injl i)'
2020-10-05 20:35:29 → raehik joins (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net)
2020-10-05 20:35:48 <ski> but we realize now that for `injr', we need to induct on `m' as well. so let's define `injr j : Fin (m + n)' in terms of `m + j : Fin (m + n)', where `Z + j = j; S m + j = S (m + j)'
2020-10-05 20:35:59 <sep2> Did I translate transition over correctly? https://dpaste.org/u84O
2020-10-05 20:36:06 <sep2> For letter
2020-10-05 20:36:32 <ski> we really need to induct on `m' here, not `j', since we need to rewrite the `m + n' in the type to something of the form `S (...)' to be able to use the data constructors of `Fin'
2020-10-05 20:37:03 <ski> sep2 : what's the final state ?
2020-10-05 20:37:08 × Franciman quits (~francesco@host-212-171-42-250.retail.telecomitalia.it) (Quit: Leaving)
2020-10-05 20:38:04 × snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 265 seconds)
2020-10-05 20:38:07 <ski> (if we have some kind of subtyping, we could allow `i : Fin (m + n)' if `i : Fin m', eliding the explicit `injl' call which just "copies" the constructors anyway)
2020-10-05 20:38:37 <tomsmeding> there is no single definition of + which makes both injl and injr natural, right
2020-10-05 20:38:52 <sep2> :ski final state should be {a}
2020-10-05 20:39:10 → Franciman joins (~francesco@host-212-171-42-250.retail.telecomitalia.it)
2020-10-05 20:39:11 <sep2> • Q={ε,a,T} •. s=ε • F = {a}
2020-10-05 20:39:13 <tomsmeding> so for choosing a definition of +, you'd have to look for a different motivation :p
2020-10-05 20:39:45 <ski> so, the effect of this is that, if we list the elements of say `Fin (3 + 5)', from least element, to greatest, we start with the elements corresponding to `Fin 3', being (using syntactic sugar) `0',`1',`2', and then comes the elements corresponding to `Fin 5', that is `3 + 0',`3 + 1',`3 + 2',`3 + 3',`3 + 4'
2020-10-05 20:40:13 <ski> sep2 : you have listed zero states (empty list), for your list of final states
2020-10-05 20:40:32 × kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection)
2020-10-05 20:41:02 <ski> tomsmeding : i think it's reasonable, for `Either a b', if we're listing the elements of it, to list the elements coming from `a' to the left of the elements coming from `b' (since `a' occurs to the left of `b' in the type)
2020-10-05 20:41:48 <ski> and combining that with wanting to start from the least element, counting upwards as we're going to the right, forces this particular version of `+' (inducting on left operand)
2020-10-05 20:41:48 <tomsmeding> kind of?
2020-10-05 20:41:56 <ski> yea
2020-10-05 20:42:18 <tomsmeding> I find the motivation kind of far-fetched, but sure :p
2020-10-05 20:42:25 × justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 240 seconds)
2020-10-05 20:42:42 <tomsmeding> it does invoke the kind of asymmetry you were looking for :p
2020-10-05 20:42:56 <ski> the premiss is somewhat weak, i agree. but it's the rationale that i've been able to find, so far, for preferring one over the other
2020-10-05 20:43:09 <tomsmeding> though maybe I'm understating the importance of Fin in dependent-typed programming
2020-10-05 20:43:19 <tomsmeding> s/understating/underestimating/
2020-10-05 20:44:20 <sep2> ski: with [1] ? [0] would indicate how many states but not which state?
2020-10-05 20:44:31 <ski> btw, note that `Fin m + Fin n = Fin (m + n)' expresses both injections (in the left-to-right direction), but also expresses a "try to subtract `m', either discovering that the input was less than `m', or else getting a difference that's less than `n'"
2020-10-05 20:44:37 × Franciman quits (~francesco@host-212-171-42-250.retail.telecomitalia.it) (Ping timeout: 264 seconds)
2020-10-05 20:45:17 <ski> sep2 : `0' is the way you're writing/encoding the starting state ⌜ε⌝, in Haskell
2020-10-05 20:45:46 <sep2> https://dpaste.org/5G3N
2020-10-05 20:45:50 → justanotheruser joins (~justanoth@unaffiliated/justanotheruser)
2020-10-05 20:46:22 <sep2> hold on
2020-10-05 20:47:11 <ski> (similarly, `Fin m * Fin n = Fin (m * n)' expresses converting between a "coordinate pair in a rectangle" and a "running index in a rectangle". in one case, it's `(i,j) |-> i * n + j', in the other it's `k |-> (k / n,k % n)')
2020-10-05 20:48:10 <ski> (and then, `(Fin m -> Fin n) = Fun (n ^ m)' is about converting between a number, and its digits, in a positional number system of base `n', having at most `m' digits)
2020-10-05 20:49:08 <tomsmeding> neat
2020-10-05 20:49:18 <ski> sep2 : `M = (states,starts,finals,transitions)' is an explanation of the rôles the different components in your quadruple, describing a finite state machine, play
2020-10-05 20:49:38 <tomsmeding> rôles
2020-10-05 20:49:47 <ski> one interesting thing about this is that, in this setting "division by zero" is not a problem :)
2020-10-05 20:49:56 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2020-10-05 20:50:02 → shadowdao joins (~user@unaffiliated/shadowdaemon)
2020-10-05 20:50:18 <tomsmeding> certainly so :p
2020-10-05 20:50:39 <sep2> ski: so when I used [1] for final state it was saying 0,1 are final states?
2020-10-05 20:50:50 <ski> i still haven't convinced myself whether to induct on left or right, for multiplication (although i'm heavily leaning towards left)
2020-10-05 20:51:11 <ski> (but that's the version i assumed, when i wrote `i * n + j', rather than `i + m * j')
2020-10-05 20:51:14 × GyroW quits (~GyroW@unaffiliated/gyrow) (Quit: Someone ate my pie)
2020-10-05 20:51:24 → GyroW joins (~GyroW@d54c03e98.access.telenet.be)
2020-10-05 20:51:24 × GyroW quits (~GyroW@d54c03e98.access.telenet.be) (Changing host)
2020-10-05 20:51:24 → GyroW joins (~GyroW@unaffiliated/gyrow)
2020-10-05 20:52:01 <tomsmeding> (or `n * i + j')
2020-10-05 20:53:14 → pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net)
2020-10-05 20:53:27 → Franciman joins (~francesco@host-212-171-42-250.pool212171.interbusiness.it)
2020-10-05 20:53:49 × caubert quits (~caubert@82.131.52.222.cable.starman.ee) (Remote host closed the connection)
2020-10-05 20:54:23 <ski> (then one can go on to have equalities/isomorphisms like `Sym (Fin n) = Fin (n !)', where `Sym A' is set of permutations (or (`Set') automorphisms, if you prefer) on `A'. it forms a group, the symmetric group, hence `Sym'. or `Sub (Fin n) (Fin k) = Fin (C n k)', where `C' is binomial coefficient, and `Sub A B' is set of `B'-sized subsets of `A' ..)
2020-10-05 20:54:33 → snakemasterflex joins (~snakemast@213.100.206.23)
2020-10-05 20:54:38 → caubert joins (~caubert@82.131.52.222.cable.starman.ee)
2020-10-05 20:55:25 → hexfive joins (~hexfive@50.35.90.193)
2020-10-05 20:55:30 <ski> tomsmeding : yes, but if `+' is doing induction on left parameter, then `n * i + j' will have to traverse `n * i' (which could be quite large), rather than just `j' (which is less than `n')
2020-10-05 20:55:50 × mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 256 seconds)
2020-10-05 20:56:13 <tomsmeding> I know, just noting that i*n+j and i+m*j are not the only options :p
2020-10-05 20:56:14 <ski> (hm, at least if we interpret `n * i + j' as `(n * i) + j' .. rather than as a ternary (mixfix) operation)
2020-10-05 20:56:20 <tomsmeding> lol
2020-10-05 20:56:25 <ski> yea, good point
2020-10-05 20:56:26 <tomsmeding> let's not go there
2020-10-05 20:57:01 <ski> sep2 : if you only specify `1' as final state, then that's the only final state that you've specified ..
2020-10-05 20:57:04 <ski> (a truism, i know)
2020-10-05 20:57:14 × hexfive quits (~hexfive@50.35.90.193) (Client Quit)
2020-10-05 20:57:20 tomsmeding . o O ( :D )
2020-10-05 20:58:22 <ski> unless you interpret `M = (states,start,finals,transitions)' to mean that `finals' does not contain all the final states .. but that seems a bit weird to me. would you have any particular reason for such an interpretation (and how to know what the remaining final states are, then) ?
2020-10-05 20:58:42 → justan0theruser joins (~justanoth@unaffiliated/justanotheruser)
2020-10-05 20:59:29 × borne quits (~fritjof@200116b86471bb007fe01feb1760d29e.dip.versatel-1u1.de) (Ping timeout: 272 seconds)
2020-10-05 21:00:01 × Guest75545 quits (~Fare@178.162.204.214) ()
2020-10-05 21:00:27 × justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 260 seconds)
2020-10-05 21:00:30 <ski> tomsmeding : anyway .. i'm only partly thinking about this as an exercise in counting, combinatorics (and dependent types in general). the other reason is to experiment with a notation for defining equalities (isomorphisms) between types, directly, rather than via two functions, which are then shown to be inverses of each other ..
2020-10-05 21:00:37 × Aquazi quits (uid312403@gateway/web/irccloud.com/x-truwgtvpybdfvjec) (Quit: Connection closed for inactivity)
2020-10-05 21:00:52 <dolio> Why is division by zero not a problem?
2020-10-05 21:01:01 <ski> (.. and doing that has led me to want to incorporate some ideas from logic programming into the mix)
2020-10-05 21:01:10 <tomsmeding> dolio: in that k / n, k : Fin n
2020-10-05 21:01:22 <tomsmeding> um
2020-10-05 21:01:22 <tomsmeding> no
2020-10-05 21:01:39 <tomsmeding> right, k : Fin (m * n)
2020-10-05 21:01:48 <tomsmeding> and if n = 0, then Fin (m * n) = Fin 0 = <empty>
2020-10-05 21:02:26 × conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.)
2020-10-05 21:02:34 <zoom84> probably a stupid question but why is the mapping func of a functor b->a instead of a->a? Is it just to provide the flexibility of returning an output whose type is different from input?
2020-10-05 21:02:50 <Cheery> how about including (Maybe a) right in your algebra and making it closed over Nothing?
2020-10-05 21:03:32 × Franciman quits (~francesco@host-212-171-42-250.pool212171.interbusiness.it) (Quit: Leaving)
2020-10-05 21:03:54 <sep2> ski: [1] gives me 1 and empty list rather than 1?
2020-10-05 21:04:13 <ski> dolio : given `k : Fin (m * n)' we want to define `k / n : Fin m' and `k % n : Fin n'. we attempt to subtract `n' from `k', repeatedly, until we know `k < n'. but we have an upper bound on the number of subtractions (that's `m'), so we can't get stuck in an infinite loop. also, if `n' is zero, then `k' with `k < n' is impossible (and then `m * n = m * 0 = 0', so `k < m * n' was also impossible, to begin with)
←Prev  Next→
Page 1 .. 442 443 444 445 446 447 448 449 450 451 452 .. 5022

All times are in UTC.