Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 126 127 128 129 130 131 132 133 134 135 136 .. 5022
— 502,152 events total
2020-09-22 03:21:42 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-22 03:23:31 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-22 03:24:40 → adamwespiser joins (~adam_wesp@209.6.42.110)
2020-09-22 03:25:12 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-09-22 03:28:22 × thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-22 03:35:21 × dirediresalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection)
2020-09-22 03:35:46 → dirediresalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt)
2020-09-22 03:37:44 × reppertj quits (~textual@pool-96-246-209-59.nycmny.fios.verizon.net) (Quit: Textual IRC Client: www.textualapp.com)
2020-09-22 03:40:44 → fresheyeball joins (~isaac@c-71-237-105-37.hsd1.co.comcast.net)
2020-09-22 03:41:30 × zacts quits (~zacts@dragora/developer/zacts) (Ping timeout: 272 seconds)
2020-09-22 03:41:30 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
2020-09-22 03:42:24 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-09-22 03:46:52 → vicfred joins (~vicfred@unaffiliated/vicfred)
2020-09-22 03:47:36 × DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Quit: Leaving...)
2020-09-22 03:47:43 × gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 272 seconds)
2020-09-22 03:49:51 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-22 03:50:26 → abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net)
2020-09-22 03:50:29 → DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-09-22 03:54:35 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2020-09-22 03:54:37 × flex14 quits (~flex14@2601:280:c780:7ea0:d233:9ddf:c010:c113) (Ping timeout: 260 seconds)
2020-09-22 03:54:52 → macrover joins (~macrover@ip70-189-231-35.lv.lv.cox.net)
2020-09-22 03:55:18 × ericsagnes quits (~ericsagne@2405:6580:0:5100:25d0:9c91:85b6:2191) (Ping timeout: 246 seconds)
2020-09-22 03:55:57 × Amras quits (~Amras@unaffiliated/amras0000) (Ping timeout: 272 seconds)
2020-09-22 04:00:32 <edwardk> i now have managed to figure out how to take the library of singleton types i have, build a category of arrows that take Sing a -> Sing b , show that is really SingI a => Sing b and has composition, where the kinds act as a sort of fiber over the terms in the language. Then I can build a category -># of the fibers, basically indexed by the kinds of the arguments in the polykinded category of functions between singletons (which
2020-09-22 04:00:32 <edwardk> acts like the constraints package on steroids) and get all haskell functions
2020-09-22 04:01:10 → sepi joins (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net)
2020-09-22 04:01:39 <edwardk> now I want to clean up the presentation to make it clearer that the latter category of finers where arrows from i -> j are (forall (a::i). (Sing a -> Some (Sing @j)) are themselves describable
2020-09-22 04:01:44 <edwardk> er fibers
2020-09-22 04:01:47 × DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Quit: Leaving...)
2020-09-22 04:02:25 <edwardk> which then recovers richard's work in the singletons library, but with my own weird spin
2020-09-22 04:02:58 hackage flink-statefulfun 0.2.0.0 - Flink stateful functions SDK https://hackage.haskell.org/package/flink-statefulfun-0.2.0.0 (tdbgamer)
2020-09-22 04:03:11 → palancovich99 joins (~ranc199@2800:a4:17ce:600:bdde:ea99:e9ec:7574)
2020-09-22 04:03:57 → ericsagnes joins (~ericsagne@2405:6580:0:5100:1d6:8b82:83b6:a62b)
2020-09-22 04:05:51 <edwardk> i guess what i really need is singletons for 'Some f'
2020-09-22 04:05:53 → sand_dull joins (~theuser@62.182.99.37)
2020-09-22 04:06:11 × unlink2 quits (~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de) (Remote host closed the connection)
2020-09-22 04:06:22 <MarcelineVQ> Sounds like you're having fun
2020-09-22 04:06:30 → unlink2 joins (~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de)
2020-09-22 04:06:35 <edwardk> generally, yes =)
2020-09-22 04:07:08 <edwardk> i have one bottleneck with my current approach
2020-09-22 04:07:28 × palancovich99 quits (~ranc199@2800:a4:17ce:600:bdde:ea99:e9ec:7574) (Quit: Leaving)
2020-09-22 04:07:38 → machinedgod joins (~machinedg@d67-193-126-196.home3.cgocable.net)
2020-09-22 04:07:47 <edwardk> i'd like to take types of kind (i -> j) and treat them at the value level as i do types of kind Type, which is as typereps for Type, here i'd want them to be typereps for types of kind (i -> j)
2020-09-22 04:07:50 → DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-09-22 04:08:44 <edwardk> but my reflection does 'on the nose' translations from types to terms, and that would mean that fromSing :: Sing (Maybe :: Type -> Type) -> Type -> Type
2020-09-22 04:08:50 <edwardk> hrmm, maybe that checks out
2020-09-22 04:09:26 <edwardk> except now i need to figure out what higher order functions look like
2020-09-22 04:10:39 <sepi> https://dpaste.org/AbtT currently trying to move onto the next element if there is no "match", [] is a placeholder, a little stuck, Any tips?
2020-09-22 04:10:51 → day_ joins (~Unknown@unaffiliated/day)
2020-09-22 04:10:57 × polyphem quits (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) (Ping timeout: 260 seconds)
2020-09-22 04:12:05 <edwardk> But I need to be able to represent singletons for kind (i -> Type) at the least to make headway on talking about Some f in general, or Some (Sing @k) -- in particular
2020-09-22 04:12:31 <edwardk> i have two existing types that look like Some x for different choices of x now. Constraint looks like Some Dict, and Type looks like Some TypeRep
2020-09-22 04:12:59 → werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net)
2020-09-22 04:13:40 <edwardk> so this does seem to indicate what a singleton looks like here
2020-09-22 04:13:53 <edwardk> Sing (a :: Type) ~ TypeRep (a :: Type)
2020-09-22 04:14:07 <edwardk> Sing (a :: Constraint) ~ Dict (a :: Constraint)
2020-09-22 04:14:26 × day quits (~Unknown@unaffiliated/day) (Ping timeout: 260 seconds)
2020-09-22 04:14:26 day_ is now known as day
2020-09-22 04:14:27 × dolio quits (~dolio@haskell/developer/dolio) (Quit: ZNC 1.8.1 - https://znc.in)
2020-09-22 04:15:10 × spew quits (uid195861@gateway/web/irccloud.com/x-qrcclbtlqeexxgus) (Quit: Connection closed for inactivity)
2020-09-22 04:15:14 → shafox joins (~shafox@106.51.234.111)
2020-09-22 04:15:33 <edwardk> but i want to be able to talk about Sing (Eq :: Type -> Constraint) or Sing (Maybe :: Type -> Type)
2020-09-22 04:18:21 → dolio joins (~dolio@haskell/developer/dolio)
2020-09-22 04:18:28 × dolio quits (~dolio@haskell/developer/dolio) (Remote host closed the connection)
2020-09-22 04:18:38 × sleblanc quits (~sleblanc@unaffiliated/sebleblanc) (Ping timeout: 260 seconds)
2020-09-22 04:18:49 <MarcelineVQ> Any particular goal with being able to have constraints there?
2020-09-22 04:18:54 Axman6 stocks up on non-perishable food and supplies in case edwardk unlocks something truly disasterous for the planet
2020-09-22 04:19:04 <edwardk> ok, so the problem with the type rep story is i can compare TypeRep (a :: Type -> Type) for equality with another TypeRep (a :: Type -> Type) -- but i can't do that with the Type -> Type encoding
2020-09-22 04:19:07 <edwardk> yes!
2020-09-22 04:19:14 <edwardk> this makes Sing become Dict
2020-09-22 04:19:23 <Axman6> see, he's a madman
2020-09-22 04:19:34 <edwardk> just like TypeRep for Type makes Sing become TypeRep
2020-09-22 04:19:55 <edwardk> and making Nat ~ Natural lets me not have to change types between types/terms and can make round tripping through singletons O(1) not O(n)
2020-09-22 04:20:06 <edwardk> each one of these extends the space of operations i can do in constant time
2020-09-22 04:20:21 <edwardk> but since constraints are thin, they go into Sing
2020-09-22 04:20:23 → dolio joins (~dolio@haskell/developer/dolio)
2020-09-22 04:20:25 <edwardk> so does p :- q
2020-09-22 04:20:28 <edwardk> that has a singleton type
2020-09-22 04:20:29 × dolio quits (~dolio@haskell/developer/dolio) (Remote host closed the connection)
2020-09-22 04:20:53 <edwardk> so the arrows between singletons _also_ has a singleton type, because you can view them as SingI p :- SingI q
2020-09-22 04:20:59 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-22 04:21:13 <edwardk> so any function that acts on some singleton to build another passes the test
2020-09-22 04:21:33 <edwardk> so we get one category that generalizes Constraint, but which can also be used to tear apart terms
2020-09-22 04:21:42 <edwardk> and then i can look at all the fibers over it at kind Type, and we recover Hask
2020-09-22 04:22:12 <edwardk> and the way that => works, because we can view the left hand side of => and just Sing.. using the same vocabulary we do
2020-09-22 04:22:25 <edwardk> which motivates core treating constraints as thin, but still using them like types
2020-09-22 04:22:37 <edwardk> its just missing a layer of singleton type conversions to keep it sound
2020-09-22 04:23:35 → dolio joins (~dolio@haskell/developer/dolio)
2020-09-22 04:23:37 <edwardk> but i can only get away with my sort of 'homoiconic' Sing representation that has no overhead so long as all my types hold on the nose
2020-09-22 04:23:55 <edwardk> it works great right up til this need to lower terms of kind (i -> j)
2020-09-22 04:24:21 <edwardk> but I could get away there with a Demoted typeclass
2020-09-22 04:24:25 <edwardk> er
2020-09-22 04:24:27 <edwardk> type family
2020-09-22 04:24:33 <edwardk> just like is used in singletons
2020-09-22 04:24:44 <edwardk> but then it'll infect everything else i write
2020-09-22 04:25:33 <MarcelineVQ> What does thin used here mean? without inhabitants?
2020-09-22 04:25:34 <edwardk> basically type inference for the whole types lib goes to hell
2020-09-22 04:25:46 <edwardk> a thin category is one where between any two objects there is at most one arrow
2020-09-22 04:26:01 <edwardk> the category of constraints is thin (ignoring ImplicitParam fuckery)
2020-09-22 04:26:11 <edwardk> any partial order is thin viewed as -> = (<=)
←Prev  Next→
Page 1 .. 126 127 128 129 130 131 132 133 134 135 136 .. 5022

All times are in UTC.