Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 443 444 445 446 447 448 449 450 451 452 453 .. 5022
— 502,152 events total
2020-10-05 21:04:33 × caubert quits (~caubert@82.131.52.222.cable.starman.ee) (Remote host closed the connection)
2020-10-05 21:05:51 <ski> zoom84 : yes. it's "just" that
2020-10-05 21:05:58 <ski> (that's not a small thing, btw)
2020-10-05 21:06:08 → conal joins (~conal@64.71.133.70)
2020-10-05 21:06:17 <zoom84> is there a built-in version that uses a->a instead? or would I have to write my own?
2020-10-05 21:06:22 → Franciman joins (~francesco@host-212-171-42-250.pool212171.interbusiness.it)
2020-10-05 21:06:28 <ski> (also, the mathematical concept of "functor", that Haskell's `Functor' is modelled after / inspired by, requires that flexibility)
2020-10-05 21:06:47 <tomsmeding> zoom84: b->a can also be used as a->a :p
2020-10-05 21:07:11 <tomsmeding> > fmap (+1) [1..5]
2020-10-05 21:07:13 <lambdabot> [2,3,4,5,6]
2020-10-05 21:07:29 <ski> zoom84 : <https://hackage.haskell.org/package/mono-traversable-1.0.15.1/docs/Data-MonoTraversable.html#t:MonoFunctor>
2020-10-05 21:07:42 <dolio> Oh, I see. Dividing an element of the finite set by a factor of the index.
2020-10-05 21:07:47 × cosimone quits (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774) (Remote host closed the connection)
2020-10-05 21:07:55 × ericsagnes quits (~ericsagne@2405:6580:0:5100:e0:d1d9:7c60:99ac) (Ping timeout: 240 seconds)
2020-10-05 21:08:07 → cosimone joins (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774)
2020-10-05 21:08:13 <zoom84> tomsmeding, Understood. But an a->a version would permit more flexibility, such as for constructors that take two values of the same type
2020-10-05 21:08:26 <ski> sep2 : what do you mean by "[1] gives me 1 and empty list rather than 1?" ? i don't understand the question
2020-10-05 21:08:39 <zoom84> thanks for the link @ski
2020-10-05 21:08:40 × coot quits (~coot@37.30.49.218.nat.umts.dynamic.t-mobile.pl) (Quit: coot)
2020-10-05 21:08:48 <tomsmeding> zoom84: if you have a type that can _only_ support an a->a operation, then indeed the link by ski
2020-10-05 21:08:59 <ski> zoom84 : if you define `data Pair a = MkPair a a', then you can easily make an `instance Functor Pair where ...'
2020-10-05 21:09:17 <tomsmeding> yes that :p
2020-10-05 21:10:03 <ski> `MonoFunctor' is when your data type forces a particular "element type"
2020-10-05 21:10:26 <tomsmeding> or, I guess, for stuff like Set?
2020-10-05 21:10:28 <sep2> ski: my final state is [1], and you let me know that there's two final states in that
2020-10-05 21:10:35 <tomsmeding> though MonoFunctor is not really the right restriction there
2020-10-05 21:10:42 <ski> `Functor' is when your data type is parametric, allows the user of it to specify which "element type" they want to use (and so then it's useful to be able to switch from one "element type" to another)
2020-10-05 21:10:58 × cosimone quits (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774) (Remote host closed the connection)
2020-10-05 21:11:18 → cosimone joins (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774)
2020-10-05 21:11:22 <ski> <sep2> • Q={ε,a,T} •. s=ε • F = {a}
2020-10-05 21:11:38 <ski> sep2 : could you explain what is ⌜a⌝ here ?
2020-10-05 21:13:27 <dsal> fmap for `->` is just `.` isn't it?
2020-10-05 21:13:38 <ski> yes
2020-10-05 21:14:08 <tomsmeding> which belongs in the list of niceties together with ($) = id
2020-10-05 21:14:11 <ski> fmap :: (a -> b) -> ((rho ->) a -> (rho ->) b)
2020-10-05 21:15:25 → Guest89 joins (ae15459e@gateway/web/cgi-irc/kiwiirc.com/ip.174.21.69.158)
2020-10-05 21:15:38 <ski> it used to be the case, in lambdabot, that `(.)' was defined as `(.) = fmap' (with the general type, yes). also with `flip fs a = fmap ($ a) fs'
2020-10-05 21:15:50 × Guest89 quits (ae15459e@gateway/web/cgi-irc/kiwiirc.com/ip.174.21.69.158) (Client Quit)
2020-10-05 21:16:00 <ski> @type let flip fs a = fmap ($ a) fs in flip
2020-10-05 21:16:01 <lambdabot> Functor f => f (a -> b) -> a -> f b
2020-10-05 21:16:37 <ski> so you could say `flip [(2 +),(2 *),(2 ^)] 3', e.g.
2020-10-05 21:16:42 × shafox quits (~shafox@106.51.234.111) (Remote host closed the connection)
2020-10-05 21:17:09 <ski> > [(2 +),(2 *),(2 ^)] `sequence` 3 -- another way to get the same thing
2020-10-05 21:17:12 <lambdabot> [5,6,8]
2020-10-05 21:18:19 <ski> zoom84 : did you try making such an instance for `Pair', perhaps ?
2020-10-05 21:18:30 <sep2> ski: I had the thought that I just fill in the numbers for a espilon, a, T so I used 0,1,2
2020-10-05 21:18:42 → bbear joins (~dkremer@2a01:e34:ec2b:d430:cc93:67b2:c4ea:7463)
2020-10-05 21:18:50 <ski> sep2 : is ⌜a⌝ a state ?, is ⌜T⌝ a state ?
2020-10-05 21:18:52 <dolio> ski: That seems kind of like the 'division' equivalent of the type theoretic 'axiom of choice'.
2020-10-05 21:19:10 × snakemasterflex quits (~snakemast@213.100.206.23) (Ping timeout: 246 seconds)
2020-10-05 21:19:20 <ski> dolio : hm, which ?
2020-10-05 21:19:36 <tomsmeding> ski: that's an... interesting definition of 'flip'
2020-10-05 21:19:53 <ski> > sequence ["ab","012"] -- you mean this ?
2020-10-05 21:19:55 <lambdabot> ["a0","a1","a2","b0","b1","b2"]
2020-10-05 21:20:09 <ski> tomsmeding : actually, i recall seeing it in a math paper :)
2020-10-05 21:20:26 → ericsagnes joins (~ericsagne@2405:6580:0:5100:a920:8792:1be2:949f)
2020-10-05 21:20:27 <dolio> ski: By that I mean, what is sometimes called 'the axiom of choice' is just rearranging a choice that has already been made. :)
2020-10-05 21:20:50 <ski> dolio : yes. i'm just not seeing the relation to what was discussed above
2020-10-05 21:20:55 <monochrom> Ha, I like that, dolio. :)
2020-10-05 21:20:58 <tomsmeding> Like sure, the function is nice, but why call it 'flip' :p
2020-10-05 21:20:58 <dolio> And this 'divide by zero' is obligated to provide the other factor of 0 as a premise.
2020-10-05 21:21:03 → jesusabdullah joins (~jesusabdu@178.162.204.214)
2020-10-05 21:21:38 <zoom84> :r
2020-10-05 21:22:03 <ski> (Bishop expresses it as it lying in the meaning of the existential quantifier that a choice already has been made. but then, the operation that the AoC gives you needn't be extensional wrt the equivalence relation you've specified your sets (setoids) with)
2020-10-05 21:22:43 <dolio> Right. In something like HoTT you can write a proper notion of the axiom of choice.
2020-10-05 21:23:17 <monochrom> "If I have a whole bunch of non-empty sets" --- sounds like for each set there, I have already chosen an element. "then their cartesian product is non-empty" --- use the aforementioned chosen elements to form the desired sequence. What can possibly go wrong? :)
2020-10-05 21:23:42 ski . o O ( "Intensional vs Extensional Choice" by roconnor in 2005-06-04 at <http://r6.ca/blog/20050604T143800Z.html> )
2020-10-05 21:23:47 <dolio> Without having to decode it into the setoid interpretation explicitly.
2020-10-05 21:24:12 → jwynn6 joins (~jwynn6@050-088-122-078.res.spectrum.com)
2020-10-05 21:24:16 → mav1 joins (~mav@p5dee344b.dip0.t-ipconnect.de)
2020-10-05 21:24:21 <sep2> ski: from what I can tell they're all states start, end and trap
2020-10-05 21:25:24 <ski> dolio : well, i think it can be blind in `m'. it's just that, if `n' is zero, then there is no `k : Fin (m * 0)', and so we can't even get to the point of evaluating `k / n'
2020-10-05 21:25:39 × cosimone quits (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774) (Remote host closed the connection)
2020-10-05 21:25:40 × Franciman quits (~francesco@host-212-171-42-250.pool212171.interbusiness.it) (Remote host closed the connection)
2020-10-05 21:25:58 → Franciman joins (~francesco@host-212-171-42-250.retail.telecomitalia.it)
2020-10-05 21:26:00 → cosimone joins (~user@2001:b07:ae5:db26:f68c:50ff:fe0b:b774)
2020-10-05 21:26:44 <dolio> But you can't call the function on `Fin i` without exhibiting a factorization of `i`.
2020-10-05 21:27:25 <ski> sep2 : i don't know the particular flavor of FSMs that you're dealing with. but `M = (states,start,finals,transitions)' only seems to mention start state and final states as being "special", from the point of view of this general FSM description. in other words, no "trap" states. in particular FSMs that you construct, you could have some other state(s ?) that you call "trap" states, though
2020-10-05 21:28:24 <ski> dolio : yea. i remember when i discovered that, years ago, i called it `skolem' (since i associated it with skolemization, not with axiom-of-choice, not sure i'd seen that formulation of it then)
2020-10-05 21:29:03 → dcabrejas joins (bcd609cc@188.214.9.204)
2020-10-05 21:29:20 <dolio> Well, I don't exactly mean it's the axiom of choice, but it's giving it the 'hard part' in a similar way.
2020-10-05 21:30:02 <ski> sep2 : so, for your particular FSM that you're trying to encode (which one is that, at the moment, `emptyFSM' or some other ?), you can have ⌜T⌝ be a "trap" state. but you never answered me whether ⌜a⌝ was also a state, or not
2020-10-05 21:31:35 <ski> dolio : i think it's likely that the reason why it's provable in type theory is related to the fact that mathematicians have regarded it as being obviously true
2020-10-05 21:31:48 → wroathe_ joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-10-05 21:32:12 × wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 244 seconds)
2020-10-05 21:32:19 <ski> (it all has to do with the interpretation one gives to "there exists". and also, from what i understand, whether one allows defining quotient sets/types)
2020-10-05 21:32:26 <dolio> Well, the problem with mathematicians is that they don't actually make the choice beforehand.
2020-10-05 21:32:39 <ski> yea, so it's a conflation of two different senses
2020-10-05 21:32:54 <ski> (that's how it looks to me, at least)
2020-10-05 21:33:15 × mirrorbird quits (~psutcliff@2a00:801:2d5:9d73:ff00:6553:d451:a276) (Quit: Leaving)
2020-10-05 21:33:16 <sep2> ski: I see a would be one of the sigmas correct
2020-10-05 21:33:28 hackage hsinspect 0.0.14 - Inspect Haskell source files. https://hackage.haskell.org/package/hsinspect-0.0.14 (tseenshe)
2020-10-05 21:33:36 <ski> sep2 : i dunno what "the sigmas" are, in your context, so i can't answer
2020-10-05 21:34:02 → mirrorbird joins (~psutcliff@2a00:801:2d5:9d73:ff00:6553:d451:a276)
2020-10-05 21:35:17 <ski> sep2 : hm, looking at your paste, perhaps `sigma' refers to your set of allowed symbols/tokens, that your FSM is meant to recognize some subset of finite words, built from such symbols, from ?
2020-10-05 21:35:53 <monochrom> ski: Nice link to roconnor's post, thanks.
2020-10-05 21:36:02 <dolio> I think the real problem with classical mathematics is that it extrapolates too much from finite things to infinite things.
2020-10-05 21:36:06 <ski> dolio : "But you can't call the function on `Fin i` without exhibiting a factorization of `i`." -- yea, good point
2020-10-05 21:36:50 <dolio> Like, excluded middle is kind of reasonable in a completely finite setting.
2020-10-05 21:37:14 <monochrom> Also, sep2's alphabet Σ is simply {'0', '1'} or {'a', 'b'}, I forgot which, but it's a fixed hardcoded alphabet.
←Prev  Next→
Page 1 .. 443 444 445 446 447 448 449 450 451 452 453 .. 5022

All times are in UTC.