Logs: liberachat/#haskell
| 2021-06-08 08:37:58 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 2021-06-08 08:40:48 | × | hmmmas quits (~chenqisu1@183.217.201.236) (Quit: Leaving.) |
| 2021-06-08 08:40:51 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2021-06-08 08:41:01 | <guest61> | f a = wrap (g 0# (unwrap a)) what's # meaning here? |
| 2021-06-08 08:41:35 | × | kmein quits (~weechat@user/kmein) (Ping timeout: 252 seconds) |
| 2021-06-08 08:41:39 | <guest61> | g :: forall a# . (Num# a#, Unwrap a ~ a#) => a# -> a# -> a# |
| 2021-06-08 08:41:42 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 2021-06-08 08:41:46 | <guest61> | what 's # here? |
| 2021-06-08 08:42:07 | × | xerox quits (~edi@user/edi) (Ping timeout: 272 seconds) |
| 2021-06-08 08:42:29 | <c_wraith> | part of identifiers/literals |
| 2021-06-08 08:42:31 | → | xerox joins (~edi@user/edi) |
| 2021-06-08 08:42:41 | → | kmein joins (~weechat@user/kmein) |
| 2021-06-08 08:42:41 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-08 08:43:18 | <guest61> | consume :: a %m -> () what's % here? |
| 2021-06-08 08:43:28 | <tomsmeding> | the # in a# and Num# is just part of the name; 0# is an unboxed int literal |
| 2021-06-08 08:43:28 | <tomsmeding> | e |
| 2021-06-08 08:43:46 | <tomsmeding> | but putting a # in names is usually meant to indicate that the thing is an unboxed type |
| 2021-06-08 08:43:46 | <guest61> | dupBool = dup @Bool what's @here? |
| 2021-06-08 08:44:02 | <tomsmeding> | the % is a linear type indication, that's very recent and new |
| 2021-06-08 08:44:07 | <tomsmeding> | the @ is a type application |
| 2021-06-08 08:44:36 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 244 seconds) |
| 2021-06-08 08:45:02 | <guest61> | is there an actuall type called Type? |
| 2021-06-08 08:45:09 | <guest61> | @hoogle Type |
| 2021-06-08 08:45:10 | <lambdabot> | Data.Kind type Type = Type |
| 2021-06-08 08:45:10 | <lambdabot> | module GHC.Exception.Type |
| 2021-06-08 08:45:10 | <lambdabot> | GHC.Exts data TYPE (a :: RuntimeRep) |
| 2021-06-08 08:45:15 | <tomsmeding> | there is a _kind_ called Type |
| 2021-06-08 08:45:44 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-08 08:45:58 | <guest61> | type Code () = '['[]] what's the ' meaning? |
| 2021-06-08 08:46:07 | <guest61> | it's valid? |
| 2021-06-08 08:46:11 | <tomsmeding> | TYPE is something completely different than Type and has to do with runtime representations of data, e.g. with unboxed types; I'm not sure there |
| 2021-06-08 08:46:51 | <tomsmeding> | the ' is to disambiguate between term-level names and names resulting from lifting with DataKinds |
| 2021-06-08 08:47:26 | <tomsmeding> | [], [1], [1,2] are term-level lists |
| 2021-06-08 08:47:53 | <tomsmeding> | [] on the type level is a "type function" with kind Type -> Type |
| 2021-06-08 08:48:06 | <tomsmeding> | [a] on the type level is a type, of lists of a's |
| 2021-06-08 08:48:32 | <boxscape> | % :i Data.Kind.Type |
| 2021-06-08 08:48:32 | <yahb> | boxscape: type Data.Kind.Type :: *; type Data.Kind.Type = TYPE 'LiftedRep; -- Defined in `GHC.Types' |
| 2021-06-08 08:48:37 | <boxscape> | that's the relationship |
| 2021-06-08 08:48:40 | <tomsmeding> | '[], '[1], '[1,2] are types of kind [Int] obtained by lifting using DataKinds |
| 2021-06-08 08:48:46 | <guest61> | Maybe (a :~: b) what's this :~: mean? |
| 2021-06-08 08:49:13 | <tomsmeding> | % :i (Data.Type.Equality.:~:) |
| 2021-06-08 08:49:13 | <yahb> | tomsmeding: type role (:~:) nominal nominal; type (:~:) :: forall {k}. k -> k -> *; data (:~:) a b where; Refl :: forall {k} (a :: k). (:~:) a a; -- Defined in `Data.Type.Equality'; infix 4 :~:; instance forall k (a :: k) (b :: k). Eq (a :~: b) -- Defined in `Data.Type.Equality'; instance forall k (a :: k) (b :: k). Ord (a :~: b) -- Defined in `Data.Type.Equality'; instance forall k (a :: k) (b :: k). (a ~ b) => |
| 2021-06-08 08:49:16 | <guest61> | so many symbols I never seen |
| 2021-06-08 08:49:22 | <boxscape> | guest61 it's a proof that a and b are equal types |
| 2021-06-08 08:49:28 | <guest61> | data type is so confused |
| 2021-06-08 08:49:29 | <tomsmeding> | @src :~: |
| 2021-06-08 08:49:29 | <lambdabot> | Source not found. Are you typing with your feet? |
| 2021-06-08 08:49:39 | <tomsmeding> | data a :~: b where Refl :: a :~: a |
| 2021-06-08 08:50:13 | × | yd502 quits (~yd502@180.168.212.6) (Ping timeout: 258 seconds) |
| 2021-06-08 08:50:54 | <tomsmeding> | guest61: I do wonder: if you're not very familiar with all the ghc extensions to haskell yet, why are you looking at unboxed types, linear types, and DataKinds? |
| 2021-06-08 08:51:12 | <tomsmeding> | I recommend getting more familiar with the language before venturing into the weeds :p |
| 2021-06-08 08:51:25 | <guest61> | tomsmeding I just a follow a haskell guy |
| 2021-06-08 08:51:28 | <tomsmeding> | assuming, of course, that it confuses and annoys you |
| 2021-06-08 08:52:14 | → | yd502 joins (~yd502@180.168.212.6) |
| 2021-06-08 08:52:20 | <guest61> | newtype a -&> b = Hyp {invoke :: (b -&> a) } what a symbol... |
| 2021-06-08 08:52:49 | <tomsmeding> | you're not talking about edward kmett, are you? |
| 2021-06-08 08:52:51 | <guest61> | I hear there's some liquid types |
| 2021-06-08 08:53:06 | <boxscape> | we're still working on gaseous types, though |
| 2021-06-08 08:53:12 | <guest61> | tomsmeding no, it's Haskell_jack |
| 2021-06-08 08:53:16 | × | xerox quits (~edi@user/edi) (Quit: leaving) |
| 2021-06-08 08:53:36 | <tomsmeding> | liquid types is an external GHC plugin that adds some kind of strong verification of Haskell code using an SMT solver |
| 2021-06-08 08:53:44 | <tomsmeding> | well, Liquid Haskell it's called |
| 2021-06-08 08:53:54 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 272 seconds) |
| 2021-06-08 08:53:54 | <guest61> | refinement type |
| 2021-06-08 08:54:16 | <tomsmeding> | boxscape: do we have solid types down, then? :p |
| 2021-06-08 08:54:25 | <boxscape> | I'd say we have a solid grasp |
| 2021-06-08 08:54:42 | × | anon quits (~anon@176.59.52.187) (Ping timeout: 252 seconds) |
| 2021-06-08 08:54:57 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-08 08:55:42 | × | wonko quits (~wjc@user/wonko) (Remote host closed the connection) |
| 2021-06-08 08:55:57 | → | BosonCollider joins (~olofs@90-227-86-119-no542.tbcn.telia.com) |
| 2021-06-08 08:56:21 | → | kiweun joins (~sheepduck@2607:fea8:2a61:4800::2dd8) |
| 2021-06-08 08:57:04 | × | sheepduck quits (~sheepduck@2607:fea8:2a60:b700::5d55) (Ping timeout: 272 seconds) |
| 2021-06-08 08:57:48 | → | zeenk joins (~zeenk@2a02:2f04:a310:b600:b098:bf18:df4d:4c41) |
| 2021-06-08 08:59:24 | → | wonko joins (~wjc@62.115.229.50) |
| 2021-06-08 09:01:37 | <guest61> | :t maybe |
| 2021-06-08 09:01:38 | <lambdabot> | b -> (a -> b) -> Maybe a -> b |
| 2021-06-08 09:02:20 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:c8e0:dbe:1fae:ffe1) (Quit: WeeChat 2.8) |
| 2021-06-08 09:02:40 | <guest61> | if b ~ IO a, then this maybe could change Maybe a to IO a, there's a name call this transform, what's its name? I forget it |
| 2021-06-08 09:02:41 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 244 seconds) |
| 2021-06-08 09:03:01 | <dminuoso> | guest61: Id call it `note` |
| 2021-06-08 09:03:21 | <guest61> | @hoogle note |
| 2021-06-08 09:03:22 | <lambdabot> | Criterion.IO.Printf note :: CritHPrintfType r => String -> r |
| 2021-06-08 09:03:22 | <lambdabot> | Control.Error.Util note :: a -> Maybe b -> Either a b |
| 2021-06-08 09:03:22 | <lambdabot> | Protolude note :: MonadError e m => e -> Maybe a -> m a |
| 2021-06-08 09:04:16 | <boxscape> | what would such a function do? |
| 2021-06-08 09:04:42 | <guest61> | dminuoso maybe change the context, that's new to me |
| 2021-06-08 09:05:25 | <guest61> | I could do Maybe a to IO (Maybe a), but it do IO a, amazing |
| 2021-06-08 09:05:31 | → | magthe joins (~magthe@c83-252-48-230.bredband.tele2.se) |
| 2021-06-08 09:06:18 | → | favonia joins (~favonia@user/favonia) |
| 2021-06-08 09:06:29 | <tomsmeding> | guest61: to do that using 'maybe' you have to give a default value in case the input is Nothing |
| 2021-06-08 09:06:40 | <guest61> | like put a bunch Maybe a into a [], then use fromJust to get [a], but funciton like this could turn Maybe a -> [a], amazing! |
| 2021-06-08 09:06:44 | <tomsmeding> | and of course if you have such a default value, it's not very surprising anymore |
| 2021-06-08 09:06:52 | <dminuoso> | guest61: If you follow my approach, you wont even need it. |
| 2021-06-08 09:07:15 | <guest61> | dminuoso which approach? |
| 2021-06-08 09:07:21 | <boxscape> | :t catMaybes |
| 2021-06-08 09:07:22 | <lambdabot> | [Maybe a] -> [a] |
| 2021-06-08 09:11:19 | × | agumonke` quits (~user@88.160.31.174) (Read error: Connection reset by peer) |
| 2021-06-08 09:11:40 | → | agumonke` joins (~user@88.160.31.174) |
| 2021-06-08 09:12:16 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 272 seconds) |
| 2021-06-08 09:15:56 | → | user2718281828 joins (~user27181@dyn-34-6.mobile.unibas.ch) |
All times are in UTC.