Logs: freenode/#haskell
| 2021-04-12 03:06:46 | <Newbievarine> | I understand I wasn't being clear in what I meant but anyway I can just name the type and a cosntructor for it use the constructor |
| 2021-04-12 03:07:39 | <dmwit> | Hm, okay. Is your problem resolved, then? |
| 2021-04-12 03:08:47 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 2021-04-12 03:09:35 | → | rdivyanshu joins (uid322626@gateway/web/irccloud.com/x-tjgowmwnssyxkqkn) |
| 2021-04-12 03:09:37 | <Newbievarine> | well, yes. unless there is some way to from an expression of type T (which is a member of typeclass TC) get an expression of type (forall a. TC a => a) without actually naming (a type that's isomorphic to) the latter type |
| 2021-04-12 03:11:45 | <dmwit> | You definitely cannot go from `T` to `forall a. TC a => a` without knowing something special about how `T` and `TC` relate. Just knowing `instance TC T` is not enough. |
| 2021-04-12 03:14:48 | <Newbievarine> | I'm not sure what you mean by having to know something special about how T and TC relate. What I did was just declare "data ExistentialType = forall a. TC a => ConstructorHere a" then the expression "t" of type T I can just rewrite as expression "ConstructorHere t" of type ExistentialType |
| 2021-04-12 03:14:52 | × | puke quits (~vroom@217.138.252.196) (Quit: puke) |
| 2021-04-12 03:15:28 | <dmwit> | `ConstructorHere (x :: T)` is not (even isomorphic to) `forall a. TC a => a`. |
| 2021-04-12 03:16:01 | <Newbievarine> | well no, not in haskell I suppose it's not.. |
| 2021-04-12 03:16:18 | <Newbievarine> | assuming you mean ExistentialType not the expression |
| 2021-04-12 03:17:40 | × | ep1ctetus quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 2021-04-12 03:17:50 | → | raym joins (~ray@45.64.220.116) |
| 2021-04-12 03:20:41 | <c_wraith> | Usually when people start asking about this, the better solution is to forget classes and existentials. You don't need to create different types to have values with different behaviors. You can just use first-class functions or records thereof, maybe closing over an environment. |
| 2021-04-12 03:21:13 | → | berberman_ joins (~berberman@unaffiliated/berberman) |
| 2021-04-12 03:21:50 | × | berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 258 seconds) |
| 2021-04-12 03:22:11 | <Newbievarine> | it's to define a function that returns a heteregenuous list |
| 2021-04-12 03:22:19 | <dmwit> | (Whoops, I was a bit imprecise there. Instead of "is not", I should have said "has a type that is not".) |
| 2021-04-12 03:22:40 | <c_wraith> | that doesn't sound like a use case for existentials at all |
| 2021-04-12 03:22:46 | <c_wraith> | that sounds like a use case for higher-rank types |
| 2021-04-12 03:22:51 | <dmwit> | Also are you sure you need a heterogeneous list? |
| 2021-04-12 03:24:29 | → | myShoggoth joins (~myShoggot@75.164.73.93) |
| 2021-04-12 03:24:55 | <Newbievarine> | I don't know about need. but it certainly makes things more straightforward |
| 2021-04-12 03:25:28 | <hololeap> | more straightforward or more similar to what you would do in other languages? |
| 2021-04-12 03:26:08 | × | GZJ0X_ quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-04-12 03:26:16 | <Newbievarine> | I don't really use other languages. not imperivative ones anyway |
| 2021-04-12 03:26:29 | → | GZJ0X_ joins (~gzj@unaffiliated/gzj) |
| 2021-04-12 03:26:58 | <hololeap> | do you really need a list that can hold *any* type, or are there a handful of types that you want to fit into it? |
| 2021-04-12 03:28:09 | <dmwit> | Huh. I'm not sure I've ever heard "heterogeneous list" and "more straightforward" in the same breath before. |
| 2021-04-12 03:28:18 | <dmwit> | Usually the benefit is something very, very different from convenience. |
| 2021-04-12 03:28:22 | <Newbievarine> | not sure why you all feel the need to be so critical of the use of existential types |
| 2021-04-12 03:28:27 | <Newbievarine> | the use is this |
| 2021-04-12 03:28:55 | <Newbievarine> | I have a typeclass with a function that maps the type in question to a heteregenous list |
| 2021-04-12 03:29:09 | <Newbievarine> | such that the type of the elements of the list belong to a certain typeclass |
| 2021-04-12 03:30:17 | <dmwit> | So far it sounds exactly like the typical beginner existential trap we're trying to warn you about. |
| 2021-04-12 03:30:36 | <Newbievarine> | what is the trap exactly? |
| 2021-04-12 03:31:04 | <dmwit> | https://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-typeclass/ |
| 2021-04-12 03:32:04 | <Newbievarine> | okay? that doesnt' apply at all to my specific circumstance |
| 2021-04-12 03:32:31 | <dmwit> | ¯\_(ツ)_/¯ you're the expert |
| 2021-04-12 03:32:47 | → | geowiesnot joins (~user@87-89-181-157.abo.bbox.fr) |
| 2021-04-12 03:33:01 | <hololeap> | i was going to say using the full gamut of haskell's features to shoot yourself in the foot by not adhering to KISS |
| 2021-04-12 03:33:46 | <Newbievarine> | existential types might be difficult from an implementation standpoint but they are one of the most elementary concepts of type theory so not sure whhy you think ti deviates from simplicity |
| 2021-04-12 03:34:02 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 2021-04-12 03:34:21 | → | ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) |
| 2021-04-12 03:34:48 | <hololeap> | well, if it's simple and you understand how to do it, then what's the problem? |
| 2021-04-12 03:34:52 | <dmwit> | Sure. And tossing in a rule to your lambda cube saying that computations can appear in types is drop-dead simple from a theory standpoint. But that doesn't mean that the code you write once you have that rule available is simple. |
| 2021-04-12 03:36:06 | <Newbievarine> | I mean, that analogy doesn't even work. because that is not drop-dead simply from a theoretical standpoint. |
| 2021-04-12 03:36:26 | <Newbievarine> | and I didn't have a problem, I just had a simple question which was how to get from an expression in the one type to the existential type |
| 2021-04-12 03:37:12 | <Newbievarine> | apparently that was an open invitation for a nonsensical lecture on how I don't need existential types. One which would've felt more in good faith if it had been preceded by a question "can you explain what you're trying to do" or something similar |
| 2021-04-12 03:38:22 | <hololeap> | fair enough. it smelled like an anti-pattern. |
| 2021-04-12 03:38:59 | × | ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 260 seconds) |
| 2021-04-12 03:39:51 | <hololeap> | very few high-quality libraries i've seen effectively use heterogenous lists, so it was important to question the necessity of it. |
| 2021-04-12 03:39:59 | → | ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) |
| 2021-04-12 03:41:10 | <hololeap> | because there may be a much more straightforward and ergonomic way to solve your problem |
| 2021-04-12 03:43:22 | <hololeap> | Newbievarine: there is cast from Data.Typeable |
| 2021-04-12 03:43:36 | <hololeap> | not sure if that helps or not |
| 2021-04-12 03:43:43 | × | ep1ctetus quits (~epictetus@ip72-194-215-136.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 2021-04-12 03:43:53 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 240 seconds) |
| 2021-04-12 03:43:58 | <Newbievarine> | hololeap: thanks |
| 2021-04-12 03:44:27 | × | ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 258 seconds) |
| 2021-04-12 03:45:39 | → | ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) |
| 2021-04-12 03:47:17 | <Newbievarine> | hololeap: and I appreciate yuor suggestion of enumerating the possibilities (I assume using constructors with a sum type) but it's not something that makes sense in this instance just from a practical standpoint |
| 2021-04-12 03:47:29 | <ski> | .. fwiw, you most probably didn't mean to go from `T' to `forall a. TC a => a' at all (but possibly to `exists a. TC a *> a', which is a very different beast. your `ExistentialType' encodes this type) |
| 2021-04-12 03:47:40 | <hololeap> | ok, yeah, that was what i was thinking |
| 2021-04-12 03:48:03 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-04-12 03:48:18 | <Newbievarine> | ski: it was my understanding that in Haskell existential types are written using the forall keyword ? |
| 2021-04-12 03:48:51 | <ski> | (e.g. note that a value of type `forall a. Show a => a' can only be a partial value) |
| 2021-04-12 03:48:56 | <ski> | no |
| 2021-04-12 03:49:11 | <ski> | that's a misunderstanding |
| 2021-04-12 03:49:34 | <ski> | strictly speaking, existential types aren't written at all, in Haskell (including extensions) |
| 2021-04-12 03:50:08 | × | waleee-cl quits (uid373333@gateway/web/irccloud.com/x-cppcunbrtpbtpgrh) (Quit: Connection closed for inactivity) |
| 2021-04-12 03:50:11 | × | ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 260 seconds) |
| 2021-04-12 03:50:21 | → | rekahsoft joins (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) |
| 2021-04-12 03:50:39 | × | snowflake quits (~snowflake@gateway/tor-sasl/snowflake) (Remote host closed the connection) |
| 2021-04-12 03:50:45 | <ski> | (well, iirc, LHC did support `exists' .. but only in argument type position in function types, which is the "trivial" usage of them. but GHC for sure doesn't support existential types directly) |
| 2021-04-12 03:51:10 | → | snowflake joins (~snowflake@gateway/tor-sasl/snowflake) |
| 2021-04-12 03:51:22 | → | ulfryk joins (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) |
| 2021-04-12 03:51:29 | <ski> | otoh, there's two common ways to *encode* existential types. (a) using what might be termed "existential data constructor"; (b) using a CPS/Church encoding |
| 2021-04-12 03:54:05 | <ski> | take e.g. the type `exists q. ({- empty :: -} q,{- enqueue :: -} a -> q -> q,{- dequeue :: -} q -> Maybe (q,a))', representing an implementation of queues, with elements of type `a'. `q' is a hidden/forgotten/abstract/opaque/skolem type, the representation type of queues in this implementation |
| 2021-04-12 03:55:04 | <ski> | if we want to use (a) to encode this, we should start by inventing a name for this type `exists q. (q,a -> q -> q,q -> Maybe (q,a))' (parameterizing it on `a', in this case), e.g. |
| 2021-04-12 03:55:14 | <ski> | type QueueOps a = exists q. (q,a -> q -> q,q -> Maybe (q,a)) |
| 2021-04-12 03:55:23 | × | rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 2021-04-12 03:55:37 | <ski> | however, this is still pseudo-Haskell. let's replace the synonym with a `data' type |
| 2021-04-12 03:55:43 | × | ulfryk quits (~ulfryk@2a01:4b00:872d:e600:a55a:b8e3:54cc:d8d6) (Ping timeout: 250 seconds) |
| 2021-04-12 03:55:47 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-04-12 03:55:55 | <ski> | data QueueOps a = MkQOps (exists q. (q,a -> q -> q,q -> Maybe (q,a))) |
| 2021-04-12 03:56:16 | <ski> | or, using the alternative, `GADTSyntax' style for declaring `data' types |
| 2021-04-12 03:56:22 | <ski> | data QueueOps a |
| 2021-04-12 03:56:24 | <ski> | where |
| 2021-04-12 03:56:34 | <ski> | MkQOps :: (exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> QueueOps a |
| 2021-04-12 03:56:42 | × | abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 2021-04-12 03:57:04 | <ski> | now, the thing to realize is that `(exists a. ..a..) -> ...' is equivalent to `forall a. (..a..) -> ...' |
| 2021-04-12 03:57:07 | <ski> | e.g. |
| 2021-04-12 03:57:11 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 2021-04-12 03:57:15 | <ski> | length :: forall a. ([a] -> Int) |
| 2021-04-12 03:57:22 | <ski> | conceptually is equivalent to |
| 2021-04-12 03:57:31 | <ski> | length :: (exists a. [a]) -> Int |
| 2021-04-12 03:58:31 | <ski> | the first says that, for all types `a', if we call `length' with a list of elements of type `a', we'll get an `Int' back as result. the second says that, calling `length', we get an `Int' result, provided there exists some type `a' such that the argument is a list of elements of type `a' |
| 2021-04-12 03:58:52 | <ski> | so, armed with this equivalence, we can now rephrase the `data' constructor signature |
| 2021-04-12 03:58:57 | <ski> | MkQOps :: (exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> QueueOps a |
All times are in UTC.