Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 92 93 94 95 96 97 98 99 100 101 102 .. 5022
— 502,152 events total
2020-09-20 13:14:44 <edwardk> https://github.com/ekmett/haskell/blob/master/types/src/Data/Type/Internal.hs#L435
2020-09-20 13:14:44 × bitmagie quits (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de) (Quit: bitmagie)
2020-09-20 13:14:55 → acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de)
2020-09-20 13:14:57 <edwardk> each of the patterns in there and all the ones generated by TH learn the result type
2020-09-20 13:15:05 → suppi joins (~suppi@172.246.241.246)
2020-09-20 13:15:07 <edwardk> but the result argument's kind doesn't change unlike here
2020-09-20 13:17:23 <edwardk> when working with a S that is injective, (e.g. using the data family hack) you can just write
2020-09-20 13:17:27 <edwardk> pattern SVCons :: () => (r ~ 'VCons a b) => Sing a -> Sing b -> Sing r; pattern SVCons a b <- (upSVec -> SVCons' a b) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys)
2020-09-20 13:17:31 <edwardk> like every other instance
2020-09-20 13:17:39 <edwardk> and my TH would have a hope in hell of autogenerating it
2020-09-20 13:18:41 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2020-09-20 13:19:57 × acidjnk_new2 quits (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-20 13:22:55 × PropositionJoe quits (~ConJoe@cm-84.215.192.230.getinternet.no) (Quit: Leaving)
2020-09-20 13:25:24 → kritzefitz joins (~kritzefit@212.86.56.80)
2020-09-20 13:25:26 × kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection)
2020-09-20 13:25:30 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-20 13:29:26 → jeremybennett joins (~jeremyben@185.244.214.216)
2020-09-20 13:31:18 → geekosaur joins (ae68c070@cpe-174-104-192-112.neo.res.rr.com)
2020-09-20 13:33:03 <edwardk> the main concern about dumping an S into kind Nat like that though is that you get two types that produce the same value, and i can't create a custom KnownNat instance for instance KnownNat n => KnownNat (S n) -- so i can only make an overlapping instance of SingI (S n)
2020-09-20 13:33:13 <edwardk> and overlapping makes me sad
2020-09-20 13:33:25 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2020-09-20 13:35:44 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 13:38:28 → danso joins (~dan@107-190-41-58.cpe.teksavvy.com)
2020-09-20 13:40:01 <edwardk> Cale: https://github.com/TimWSpence/stitch/blob/master/src/Language/Stitch/Exp.hs#L158
2020-09-20 13:40:04 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 246 seconds)
2020-09-20 13:40:31 <edwardk> SVec ~ Sing here
2020-09-20 13:41:08 <edwardk> TypeRep a there is Sing (a :: Type) here
2020-09-20 13:41:41 <edwardk> exprType :: Sing ctx -> Exp ctx ty -> Sing ty
2020-09-20 13:42:19 <edwardk> comes about from the types library mashing everything into one rep
2020-09-20 13:46:49 × drbean quits (~drbean@TC210-63-209-85.static.apol.com.tw) (Ping timeout: 260 seconds)
2020-09-20 13:47:07 × outerpassage quits (~outerpass@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Ping timeout: 260 seconds)
2020-09-20 13:48:58 <Cale> On the one hand, this is all kind of cool, on the other hand, it's definitely crossing the line into dependently-typed stuff that I think Haskell just plain isn't good at yet. I think if you actually need explicit singletons, that's a pretty good indication of "oops, Haskell is going to suck at this". I wonder how long until we can realistically have a working pi.
2020-09-20 13:50:24 → troydm joins (~troydm@unaffiliated/troydm)
2020-09-20 13:50:43 × polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-20 13:51:27 hackage inline-c 0.9.1.2 - Write Haskell source files including C code inline. No FFI required. https://hackage.haskell.org/package/inline-c-0.9.1.2 (FrancescoMazzoli)
2020-09-20 13:53:37 × lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Ping timeout: 264 seconds)
2020-09-20 13:55:21 → jespada joins (~jespada@148.252.133.47)
2020-09-20 13:55:34 → acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de)
2020-09-20 13:55:47 <edwardk> well, i have been building a little dependent type checker in haskell, and every time i move more stuff into my types i catch more bugs =)
2020-09-20 13:56:09 <edwardk> so i'm just trying to push a few more things into them
2020-09-20 13:56:17 <edwardk> which is what prompted the singleton push
2020-09-20 13:56:31 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 13:56:36 <edwardk> getting the singleton stuff to be super fast and more homogeneous made me happy, til Nat made me sad
2020-09-20 13:59:56 → caumeslasal joins (~Thunderbi@157.139.207.77.rev.sfr.net)
2020-09-20 14:00:29 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-20 14:00:35 × caumeslasal quits (~Thunderbi@157.139.207.77.rev.sfr.net) (Client Quit)
2020-09-20 14:00:39 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-09-20 14:01:06 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds)
2020-09-20 14:01:17 → son0p joins (~son0p@186.159.4.142)
2020-09-20 14:03:37 × kicov quits (959c7c03@nat.ds3.agh.edu.pl) (Remote host closed the connection)
2020-09-20 14:05:49 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-20 14:06:41 → gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net)
2020-09-20 14:06:53 → Ashely3 joins (5beb81b2@gateway/web/cgi-irc/kiwiirc.com/ip.91.235.129.178)
2020-09-20 14:08:36 <edwardk> i suppose what i could do is build a type data Unnat = Add Int# Nat -- relying on the fact that Int# doesn't promote so we don't have to worry about any 'native' terms in kind Unnat. use my data family trick to inject a S constructor, and one for, so that it morally models data Unnat = S Unnat | N Nat -- so i can distinguish between the base number type i got from type Nat and the number of times i called S on it
2020-09-20 14:08:56 <edwardk> that way i don't need to worry about S 1 ~ 2 causing the universe to collapse or something
2020-09-20 14:10:48 <edwardk> another another option is to just do what I do now which is use an hlist and carry a witness of the length around rather than use Vec a N
2020-09-20 14:11:05 × gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 240 seconds)
2020-09-20 14:11:16 <Cale> Also, I haven't really thought very hard about how this suggestion might help, but generally I think if you're going to use overlapping instances in order to compute things, everything is okay in the case that you can manage to avoid exporting the class.
2020-09-20 14:11:32 → polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08)
2020-09-20 14:11:38 <edwardk> the class here is a very public offering
2020-09-20 14:11:41 <Cale> yeah
2020-09-20 14:12:06 <edwardk> i was hoping to split this out and ran into this issue while writing up examples
2020-09-20 14:12:44 <edwardk> i had started looking for 'all the instances i can add to base' when i ran afoul of this
2020-09-20 14:12:47 <Cale> I don't know if there's a way to make a private analogue and get anything related to what you want (like, make a public instance for that class that depends on an instance of the class that nobody's allowed to see, maybe)
2020-09-20 14:12:49 <edwardk> er from base
2020-09-20 14:13:24 laxask is now known as sudden
2020-09-20 14:13:42 × Ashely3 quits (5beb81b2@gateway/web/cgi-irc/kiwiirc.com/ip.91.235.129.178) (Disconnected by services)
2020-09-20 14:13:46 <edwardk> i'm inclined to just yolo the data family S thing
2020-09-20 14:13:50 <edwardk> and go on with my day
2020-09-20 14:13:56 <edwardk> and if it bites anyone say 'don't do that'
2020-09-20 14:14:17 → Ashely3 joins (c247e36b@gateway/web/cgi-irc/kiwiirc.com/ip.194.71.227.107)
2020-09-20 14:14:25 × Ashely3 quits (c247e36b@gateway/web/cgi-irc/kiwiirc.com/ip.194.71.227.107) (Disconnected by services)
2020-09-20 14:15:03 <edwardk> data family S' :: Nat -> k; type S :: Nat -> Nat; type S = S' -- just works .. til you need to feed it to + and want + to actually compute, because they closed the type family for +
2020-09-20 14:15:07 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-20 14:15:17 <edwardk> but i could offer my own + and have it delegate to the main + once i changed out the S's
2020-09-20 14:15:47 <edwardk> but then the benefit of working with base Nat is fleeing fast
2020-09-20 14:17:20 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 14:17:43 × nyd quits (~nyd@unaffiliated/elysian) (Quit: nyd)
2020-09-20 14:18:31 → lagothrix joins (~lagothrix@unaffiliated/lagothrix)
2020-09-20 14:19:38 <edwardk> i want a way to export a thing only at the type level without having to infect it with a type like Type that doesn't exist as a term.
2020-09-20 14:19:52 <edwardk> where i can have constructors in it, without using my data families
2020-09-20 14:20:08 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Ping timeout: 272 seconds)
2020-09-20 14:20:52 <edwardk> leaning towards exporting my own Nat type, ignoring the TypeNats Nat and going on my way.
2020-09-20 14:21:19 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-20 14:21:47 <edwardk> since Natural currently doesn't promote i _could_ use the data family hack to put Z and S in it as a kind.
2020-09-20 14:21:52 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2020-09-20 14:22:15 <edwardk> then you could use linear time slow SingI instances if you had to
2020-09-20 14:23:16 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-09-20 14:23:17 <edwardk> and i'd have both Nat and Natural, with the former working for when i want a large literal and the latter when i want induction for things like environments that'll usually get built from 0, til... next ghc release or so when they merge Nat and Natural
2020-09-20 14:23:28 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-20 14:24:01 <edwardk> to make the linear time thing less awful, i could emulate a better basis, like binary nats, or zeroless binary or something.
2020-09-20 14:25:04 → bloodstalker joins (~bloodstal@46.166.187.178)
2020-09-20 14:25:09 <edwardk> that'd get me log time literals, and Z and S become type families acting on the type, but they require more type information about the rest of the nat to know what to do at some points
2020-09-20 14:25:42 <edwardk> where peano can succ without forcing or matching on anything
2020-09-20 14:25:58 → __Joker joins (~Joker@180.151.105.65)
2020-09-20 14:27:05 <Cale> Yeah, how does merging Nat and Natural work with type families wanting to compute anything?
2020-09-20 14:27:11 × olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 265 seconds)
2020-09-20 14:27:18 <Cale> I mean, in the future GHC case
2020-09-20 14:27:56 → kicov joins (959c7c03@nat.ds3.agh.edu.pl)
2020-09-20 14:28:56 <Cale> I guess they just have wired in type families anyway
←Prev  Next→
Page 1 .. 92 93 94 95 96 97 98 99 100 101 102 .. 5022

All times are in UTC.