Logs: liberachat/#haskell
| 2021-08-16 07:46:20 | <superstar64> | If haskell becomes dependently typed, what happens to the kind of `(->)`? does it stay as `Type -> Type -> Type`? |
| 2021-08-16 07:46:20 | → | MatrixTravelerbo joins (~voyagert2@2001:470:69fc:105::22) |
| 2021-08-16 07:46:20 | → | ServerStatsDisco joins (~serversta@2001:470:69fc:105::1a) |
| 2021-08-16 07:46:22 | × | cjb quits (~cjb@user/cjb) (Quit: rcirc on GNU Emacs 28.0.50) |
| 2021-08-16 07:49:10 | <joel135> | Not an expert but I'd guess yes |
| 2021-08-16 07:49:18 | × | hnOsmium0001 quits (uid453710@id-453710.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-08-16 07:49:37 | jjhoo_ | is now known as jjhoo |
| 2021-08-16 07:50:02 | <keutoi> | depends on the hierarchy of universes |
| 2021-08-16 07:50:58 | → | Boomerang joins (~Boomerang@xd520f68c.cust.hiper.dk) |
| 2021-08-16 07:51:21 | <keutoi> | idris or agda models |
| 2021-08-16 07:51:53 | <joel135> | The possible objections are 1) need to distinguish universe levels Type n but seems unnecessary if the language is not supposed to be terminating/consistent, 2) A -> B might be replaced by (x : A) -> B |
| 2021-08-16 07:53:24 | <Axman6> | curious what the kind of (->) in replicate :: (n :: Int) -> a -> Vec n a would have now |
| 2021-08-16 07:53:29 | <joel135> | or (_ : A) -> B, but in the end this may then still be written just A -> B, in particular Type -> Type |
| 2021-08-16 07:53:34 | <Axman6> | Not evenm sure how to write those types |
| 2021-08-16 07:55:30 | <superstar64> | If dependent (->) is a pair of a type and a type bound by a type, wouldn't it be something like `Type -> (Type -> Type) -> Type` |
| 2021-08-16 07:56:36 | <superstar64> | or am i confusing things? |
| 2021-08-16 07:56:51 | <joel135> | 3) The dependent version of _->_ is not really a type constructor, but modulo binding issues it can be approximated like you just wrote superstar64 |
| 2021-08-16 07:57:58 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-16 07:58:52 | <joel135> | (If by 'type constructor' one insists that it should work like any type constructor of two arguments, not meddling with binding) |
| 2021-08-16 08:00:00 | <superstar64> | can you abstract `(x : A) -> B` into `(->) A (\x -> B)? |
| 2021-08-16 08:00:18 | <joel135> | Actually you may be confusing things just a little. It would be `(A : Type) -> (A -> Type) -> Type` |
| 2021-08-16 08:00:54 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-08-16 08:01:09 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 2021-08-16 08:02:21 | <joel135> | You can, if the latter (->) has a slightly different definition than the former -> . It needs to 'internalize' the binding of x : A somehow. |
| 2021-08-16 08:04:16 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 2021-08-16 08:04:22 | → | jgeerds joins (~jgeerds@55d45555.access.ecotel.net) |
| 2021-08-16 08:04:40 | <joel135> | (\x -> B) does have type (x : A) -> B a.k.a. (\x -> B), so all is good there |
| 2021-08-16 08:05:37 | <joel135> | err scratch the last message |
| 2021-08-16 08:05:51 | → | hendursa1 joins (~weechat@user/hendursaga) |
| 2021-08-16 08:06:25 | lep- | is now known as lep |
| 2021-08-16 08:07:26 | <joel135> | I meant your type `\x -> B` does have my type (or kind) `A -> Type`, which is good |
| 2021-08-16 08:07:53 | <superstar64> | I really need to stop winging it with language design and actually read some type theory book |
| 2021-08-16 08:08:42 | <joel135> | Have you tried some agda? It is pretty easy compared to dependent types in haskell |
| 2021-08-16 08:08:46 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 244 seconds) |
| 2021-08-16 08:08:57 | <superstar64> | Is "Type Theory & Functional programming" a good book on this stuff? |
| 2021-08-16 08:09:16 | <joel135> | I don't know |
| 2021-08-16 08:09:24 | → | kayprish joins (~kayprish@cable-188-2-229-172.dynamic.sbb.rs) |
| 2021-08-16 08:10:08 | <superstar64> | I guess I could read "Programming Language Foundations in Agda" too |
| 2021-08-16 08:10:43 | <joel135> | I recall there is some book by Pierce, and one by Harper, and then I recognize the title you just wrote too |
| 2021-08-16 08:11:28 | <joel135> | Or maybe you don't need a book, just some tutorial pdf for agda |
| 2021-08-16 08:12:18 | <superstar64> | you mean "Types and Programming Languages" and "Practical Foundations for Programming Languages" |
| 2021-08-16 08:12:41 | <superstar64> | I really just need to stop being lazy and read of these eventually |
| 2021-08-16 08:13:18 | <joel135> | I think that's them yes |
| 2021-08-16 08:13:25 | <merijn> | TaPL is *the* goto book, yes |
| 2021-08-16 08:14:23 | <superstar64> | I'm not sure if it's that useful to me. At this point I understand systme-fω and hindley milner really well. |
| 2021-08-16 08:15:02 | <superstar64> | (though I'm worried I might have knowledge gaps, I learned everything by throwing my self at papers) |
| 2021-08-16 08:17:37 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2021-08-16 08:17:37 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 2021-08-16 08:17:40 | allbery_b | is now known as geekosaur |
| 2021-08-16 08:23:43 | <gehmehgeh> | hmm, is there something like a (for lack of better terms) dynamically growing list comprehension? For example: [(x,y,z, other_variables_here) | x<-xlist, y<-ylist,z<-zlist, ... ... and so on] |
| 2021-08-16 08:24:39 | <gehmehgeh> | (Is my question understandable?) |
| 2021-08-16 08:25:41 | <lortabac> | gehmehgeh: not for me :) |
| 2021-08-16 08:25:46 | <Boomerang> | The tuple size is static right? If so you could use the Applicative instance of lists |
| 2021-08-16 08:26:03 | <Boomerang> | (,,,,) <$> xs <*> ys <*> zs <*> ... |
| 2021-08-16 08:26:40 | <gehmehgeh> | No, the tuple size is "dynamic"(tm) |
| 2021-08-16 08:27:01 | <Boomerang> | How do you control the size? |
| 2021-08-16 08:27:33 | <gehmehgeh> | well, the tuple size is finite |
| 2021-08-16 08:27:35 | <int-e> | > sequence [[0,1],[2,3],[4,5]] |
| 2021-08-16 08:27:36 | <lambdabot> | [[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]] |
| 2021-08-16 08:27:46 | <gehmehgeh> | I don't control it, tha's why I'm asking :) |
| 2021-08-16 08:27:54 | <int-e> | the list monad is a typical answer to this |
| 2021-08-16 08:27:57 | <gehmehgeh> | int-e: wow, that looks like it |
| 2021-08-16 08:28:00 | <gehmehgeh> | ! |
| 2021-08-16 08:28:12 | <gehmehgeh> | int-e: where can I learn more about this? |
| 2021-08-16 08:28:14 | <superstar64> | gehmehgeh, that's for lists though, not tuples |
| 2021-08-16 08:28:26 | <gehmehgeh> | superstar64: that's ok, too |
| 2021-08-16 08:28:41 | <superstar64> | every element in a list must have the same type, it's not quite the same |
| 2021-08-16 08:28:50 | <int-e> | superstar64: you can use lists as homogeneous (hope that's fine) variable size tuples |
| 2021-08-16 08:28:50 | <gehmehgeh> | Indeed. |
| 2021-08-16 08:29:47 | <gehmehgeh> | int-e: Question, so this only works because List (as in "[]") is a Monad? |
| 2021-08-16 08:30:00 | <gehmehgeh> | Or would it also work if it were an Applicative? |
| 2021-08-16 08:30:05 | <gehmehgeh> | (*only Applicative) |
| 2021-08-16 08:30:13 | <gehmehgeh> | I mean, there's sequenceA |
| 2021-08-16 08:30:32 | <gehmehgeh> | yep |
| 2021-08-16 08:30:36 | <gehmehgeh> | sequenceA also works |
| 2021-08-16 08:30:42 | <int-e> | gehmehgeh: https://wiki.haskell.org/Blow_your_mind has a bunch of this stuff, but is very disorganized |
| 2021-08-16 08:30:48 | × | fabfianda quits (~fabfianda@37.183.255.57) (Ping timeout: 272 seconds) |
| 2021-08-16 08:31:02 | <gehmehgeh> | int-e: I needed exactly the expression you posted in a bit of code to finish something |
| 2021-08-16 08:31:07 | <gehmehgeh> | int-e: So thanks a lot. |
| 2021-08-16 08:31:20 | → | fabfianda joins (~fabfianda@mob-5-91-112-128.net.vodafone.it) |
| 2021-08-16 08:37:03 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-08-16 08:38:08 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-16 08:38:12 | → | nsilv joins (~nsilv@host-79-17-175-58.retail.telecomitalia.it) |
| 2021-08-16 08:39:45 | <kuribas> | Shame contramap isn't in base... |
| 2021-08-16 08:39:54 | <kuribas> | :t contramap |
| 2021-08-16 08:39:55 | <lambdabot> | Contravariant f => (a -> b) -> f b -> f a |
| 2021-08-16 08:40:41 | <kuribas> | oh, it is apparently! |
| 2021-08-16 08:41:16 | → | jtomas joins (~jtomas@233.red-83-34-2.dynamicip.rima-tde.net) |
| 2021-08-16 08:46:49 | <int-e> | Hmm, GHC.TypeNats is so barebones... withNatVal :: KnownNat n => (Natural -> f n) -> f n would be convenient when only the result type of a function has the type evidence |
| 2021-08-16 08:47:40 | <int-e> | It's not difficult to write, of course: withNatVal x = let r = x (natVal r) in r |
| 2021-08-16 08:48:33 | <int-e> | (and then there's various variants involving (scoped) type variables) |
| 2021-08-16 08:54:13 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-16 08:55:00 | <kuribas> | I hope there will be production ready dependently typed language one day (not haskell). |
| 2021-08-16 08:56:10 | <tomsmeding> | I expect that will need to come with some significant advances in theory, in the direction of usability and expressiveness |
| 2021-08-16 08:56:58 | <kuribas> | I think it will be *more* usable and expressive then the complicated type hackery we do in haskell now. |
| 2021-08-16 08:57:35 | <tomsmeding> | what about, say, Idris is not yet "production ready" according to you? |
| 2021-08-16 08:57:39 | <kuribas> | The problem with a language like idris is that is unpolished, lacking in libraries for about anything, still many compiler bugs. |
| 2021-08-16 08:57:44 | <tomsmeding> | ah |
| 2021-08-16 08:57:58 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-08-16 08:58:03 | <tomsmeding> | it should have targeted the jvm /s |
All times are in UTC.