Logs: freenode/#haskell
| 2021-03-24 16:09:41 | → | Kaeipi joins (~Kaiepi@47.54.252.148) |
| 2021-03-24 16:09:45 | <tomsmeding> | or even a type family |
| 2021-03-24 16:09:55 | <tomsmeding> | I guess the usefulness of that depends on what exactly ij wants to do |
| 2021-03-24 16:09:59 | <ski> | yea |
| 2021-03-24 16:10:50 | <ij> | !unabbr FD |
| 2021-03-24 16:11:09 | <geekosaur> | functional dependency |
| 2021-03-24 16:11:16 | <tomsmeding> | MPTC = multi-parameter type classes |
| 2021-03-24 16:11:24 | <ij> | the other one is googleable |
| 2021-03-24 16:11:32 | <tomsmeding> | fair |
| 2021-03-24 16:12:51 | <ij> | I think a typeclass should be enough |
| 2021-03-24 16:13:31 | <ij> | however, if I want to put my "two datas with their instances of a typeclass", i.e. IJThing a => a inside a "data Progress", then I need existential types? |
| 2021-03-24 16:13:59 | <ski> | do you ? |
| 2021-03-24 16:14:26 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 240 seconds) |
| 2021-03-24 16:14:31 | <ij> | I thought I did |
| 2021-03-24 16:14:37 | <ski> | (also, it would be `IJThing a *> a', since `IJThing a => a' is not that useful) |
| 2021-03-24 16:14:48 | <ski> | i dunno. i don't know your requirements, what you have in mind |
| 2021-03-24 16:14:58 | <tomsmeding> | ij: would that 'a' type variable also be a type parameter of 'Progress'? |
| 2021-03-24 16:15:15 | <tomsmeding> | as in: data Progress a = Progress Something (IJThing a) SomethingElse |
| 2021-03-24 16:15:19 | <ski> | presumably not (in case it's going to encode an existential) |
| 2021-03-24 16:15:42 | <ij> | I realized I probably don't need that, I just need the typeclass functions |
| 2021-03-24 16:16:18 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 2021-03-24 16:16:28 | <tomsmeding> | ski: where is (*>) from? |
| 2021-03-24 16:16:35 | <ij> | I was also wondering |
| 2021-03-24 16:16:45 | <ski> | do you (a) ever need to be able to accept both alternatives in the same place, and determine which of the alternatives that you got; (b) perhaps only need to accept both in the same place, without needing to do a case distinction ? |
| 2021-03-24 16:16:49 | <ski> | tomsmeding : no |
| 2021-03-24 16:17:14 | <geekosaur> | @index (*>) |
| 2021-03-24 16:17:15 | <lambdabot> | Control.Applicative, Prelude |
| 2021-03-24 16:17:18 | <ski> | `*>' is to `=>' as `(,)' is to `(->)' as `exists' is to `forall' |
| 2021-03-24 16:17:28 | <geekosaur> | oh, ski'sspecial syntax again |
| 2021-03-24 16:17:53 | <tomsmeding> | can you even define that type operator? :p |
| 2021-03-24 16:17:57 | <ski> | `*>' is pseudo-Haskell syntax that i'm using, usually together with `exists', in order to more efficiently communicate and elucidate about such matters |
| 2021-03-24 16:18:00 | <ski> | ues |
| 2021-03-24 16:18:02 | <ski> | yes |
| 2021-03-24 16:18:13 | <tomsmeding> | with that semantic meaning |
| 2021-03-24 16:18:15 | <ski> | data cxt *> a = cxt => Wrap a |
| 2021-03-24 16:18:33 | <tomsmeding> | wait does that work? |
| 2021-03-24 16:18:33 | <ski> | data cxt *> a where Wrap :: cxt => a -> (cxt *> a) |
| 2021-03-24 16:18:50 | <tomsmeding> | that's cool |
| 2021-03-24 16:18:51 | <ij> | ski, (a) no, only one. don't care which, as long as typeclass functions are there (b) don't need cases |
| 2021-03-24 16:18:54 | <ski> | however, the way i'm using it, informally, it's without an explicit wrapping data constructor |
| 2021-03-24 16:18:56 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2021-03-24 16:19:26 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Quit: Lost terminal) |
| 2021-03-24 16:19:27 | <tomsmeding> | I see |
| 2021-03-24 16:19:43 | <ski> | `T -> (forall a. C a => F a)' is equivalent to `forall a. C a => (T -> F a)' |
| 2021-03-24 16:19:48 | tomsmeding | always used existentials directly |
| 2021-03-24 16:19:59 | <ski> | `(exists a. C a *> F a) -> T' is equivalent to `forall a. C a => (F a -> T)' |
| 2021-03-24 16:20:20 | <ski> | existentials don't exist in Haskell (with extensions), directly |
| 2021-03-24 16:20:20 | × | emmanuel_erc quits (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) (Read error: Connection reset by peer) |
| 2021-03-24 16:20:33 | <ski> | you have to encode them (using one of two encodings, typically) |
| 2021-03-24 16:20:35 | → | emmanuel_erc joins (~user@2603-7000-9600-01c9-0000-0000-0000-0874.res6.spectrum.com) |
| 2021-03-24 16:20:37 | <tomsmeding> | data Progress = forall a. IJThing a => Progress Something (IJThing a) SomethingElse |
| 2021-03-24 16:20:40 | <tomsmeding> | is what I was thinking about |
| 2021-03-24 16:20:44 | <ski> | (sometimes you can use a recursive type, instead) |
| 2021-03-24 16:20:52 | <tomsmeding> | you do have to wrap them |
| 2021-03-24 16:20:53 | <ij> | tomsmeding, right |
| 2021-03-24 16:20:58 | <ski> | that's the "existential data constructor" encoding |
| 2021-03-24 16:21:07 | <tomsmeding> | ski: the other being CPS? |
| 2021-03-24 16:21:12 | <ski> | yea, Church |
| 2021-03-24 16:21:17 | <tomsmeding> | yeah I see |
| 2021-03-24 16:21:33 | <ski> | however, note that `exists s. (s,s -> F s)' is `nu s. F s' |
| 2021-03-24 16:22:01 | <ski> | (just like `forall o. (F o -> o) -> o' is `mu o. F o') |
| 2021-03-24 16:22:37 | tomsmeding | knows nu and mu are greek letters |
| 2021-03-24 16:22:42 | <ij> | (I think I'll be able to write it on the weekend now) |
| 2021-03-24 16:22:54 | <ij> | tomsmeding, ski is light years ahead of me |
| 2021-03-24 16:23:22 | <ski> | ij : ok, so it sounds like you don't need GADTs, then. try with type classes (probably with FD, if you need to go MPTC. or alternatively with AT. or maybe you could use a type family instead) |
| 2021-03-24 16:23:54 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-24 16:24:04 | <ski> | tomsmeding : `mu' is least fixed-point, `nu' is greatest. `List a = mu r. 1 + a * r'. `Stream a = nu s. a * s' |
| 2021-03-24 16:24:09 | <ij> | AT being? |
| 2021-03-24 16:24:14 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-24 16:24:16 | <tomsmeding> | associated types |
| 2021-03-24 16:24:18 | <ski> | Associated Types |
| 2021-03-24 16:24:26 | <ij> | 🧐 |
| 2021-03-24 16:24:33 | <tomsmeding> | modulo capitalisation |
| 2021-03-24 16:24:50 | <ski> | Haskell blurs the distinction, by allowing infinite values everywhere. (e.g. `List a') |
| 2021-03-24 16:25:39 | <ski> | tomsmeding : `cata :: Functor f => (f o -> o) -> (Mu f -> o)' and `ana :: Functor f => (s -> f s) -> (s -> Nu f)' |
| 2021-03-24 16:25:40 | <tomsmeding> | what whould `nu r. 1 + a * r' be? |
| 2021-03-24 16:25:55 | <ski> | type of potentially finite streams |
| 2021-03-24 16:26:06 | <ski> | (iow, not necessarily infinite) |
| 2021-03-24 16:26:26 | → | Neuromancer joins (~Neuromanc@unaffiliated/neuromancer) |
| 2021-03-24 16:26:52 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-uvokrbifiycmuqdg) |
| 2021-03-24 16:26:55 | <tomsmeding> | right, so mu and nu are respectively the smallest and largest types such that the given algebraic equality holds? |
| 2021-03-24 16:26:56 | <ski> | the idea is that with `mu', we're expecting "finite depth" (if we're talking trees, we could still e.g. have infinite width, infinite branching, but each branch would be of finite depth) |
| 2021-03-24 16:26:58 | <tomsmeding> | sort-of |
| 2021-03-24 16:27:08 | <ski> | yea |
| 2021-03-24 16:27:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-24 16:28:10 | → | apeyroux joins (~alex@78.20.138.88.rev.sfr.net) |
| 2021-03-24 16:28:30 | <ski> | e.g. `length' only terminates, for finite lists. so it's a partial function, if we're considering the type also including the infinite ones. but if we're only considering the subtype with the finite ones (which is not expressible in Haskell, so it has to be in our heads, and perhaps on paper proofs, &c.), then it's total |
| 2021-03-24 16:28:48 | tomsmeding | nods |
| 2021-03-24 16:29:02 | <tomsmeding> | I don't completely follow your exists<->nu and forall<->mu equivalences though |
| 2021-03-24 16:29:14 | <ski> | @type unfoldr |
| 2021-03-24 16:29:16 | <lambdabot> | (b -> Maybe (a, b)) -> b -> [a] |
| 2021-03-24 16:29:19 | <maralorn> | Uniaika: Bumping hlint was only a minor headache (ghc-lib-parser compiles quite slow), but it is updated now and will be merged into master on friday. |
| 2021-03-24 16:29:50 | <ski> | this is `(s -> Maybe (a,s)) -> (s -> nu s. Maybe (a,s))' -- generating a possibly-finite stream |
| 2021-03-24 16:30:02 | <ij> | ski, what kind of mathematics is this? |
| 2021-03-24 16:30:59 | <ski> | by recursively expanding each "seed"/"state" `s' (starting with the initially given one), we can eliminate all of them, getting a (possibly) infinite-depth result, a (co)recursive, coinductive data type |
| 2021-03-24 16:31:15 | <tomsmeding> | right |
| 2021-03-24 16:31:37 | <tomsmeding> | would 'mu r. a * r = nu r. a * r' ? |
| 2021-03-24 16:31:39 | × | chele quits (~chele@ip5b40237d.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2021-03-24 16:32:04 | <ski> | s >---> F s >---> F (F s) >---> F (F (F s)) >---> ... >-> F (F (F (F (...))) = nu s. F s |
| 2021-03-24 16:32:19 | <ij> | corecursion sounds like parsing |
All times are in UTC.