Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 64 65 66 67 68 69 70 71 72 73 74 .. 5022
— 502,152 events total
2020-09-19 08:01:13 <siraben> oops, ((A :: *) (x :: A). x) :: Pi (A :: *). a
2020-09-19 08:01:16 <siraben> backslash
2020-09-19 08:01:35 <edwardk> (A::*).(_::A).A
2020-09-19 08:01:45 <edwardk> however you notate that pi in your syntax
2020-09-19 08:02:24 → shatriff joins (~vitaliish@176.52.219.10)
2020-09-19 08:02:41 <edwardk> Pi(A::*). is like forall a. in haskell then the next bit Pi(_::A). A is not using the variable bound so it is like a -> a in haskell
2020-09-19 08:02:42 <siraben> (lam 0 (lam 0 (Var 0))) for term, I think.
2020-09-19 08:02:54 × cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Quit: Goodbye)
2020-09-19 08:03:03 × cantstanya quits (~chatting@gateway/tor-sasl/cantstanya) (Remote host closed the connection)
2020-09-19 08:03:06 <siraben> I'm not sure how the lam smart constructor is supposed to work
2020-09-19 08:03:06 <edwardk> lam "A" $ lam "a" $ var "a"
2020-09-19 08:03:23 <phadej> fwiw, when using bound, I never really think about de bruijn indices
2020-09-19 08:03:26 × mmohammadi98126 quits (~mmohammad@5.238.164.128) (Ping timeout: 256 seconds)
2020-09-19 08:03:34 <phadej> I just truste that `abstract` makes it right
2020-09-19 08:03:38 → kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz)
2020-09-19 08:03:39 <edwardk> those numbers aren't levels, they are variable "names"
2020-09-19 08:03:43 <edwardk> you just chose to use numbers
2020-09-19 08:03:46 <siraben> Oh I see
2020-09-19 08:03:51 <edwardk> you could use strings, or text
2020-09-19 08:03:53 × toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection)
2020-09-19 08:03:59 <siraben> The problem is that it typechecks to Expr [Char], when I need Expr Int
2020-09-19 08:04:11 <edwardk> and traverse (const Nothing) -- will get you Expr Int
2020-09-19 08:04:24 <siraben> Ah, it's clear now. Ok I'll try
2020-09-19 08:05:01 <edwardk> i even export it from bound as 'closed'
2020-09-19 08:05:29 <edwardk> fromJust . closed = 'trust me i'm closed'
2020-09-19 08:05:35 → cantstanya joins (~chatting@gateway/tor-sasl/cantstanya)
2020-09-19 08:05:54 → cosimone joins (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6)
2020-09-19 08:06:15 × drbean quits (~drbean@TC210-63-209-205.static.apol.com.tw) (Read error: Connection reset by peer)
2020-09-19 08:06:48 <edwardk> so you should be checking lam "A" $ lam "a" $ var "a". against type Pi "A" Star $ Pi "_" (Var "A") $ Var "A"
2020-09-19 08:06:58 → Lycurgus joins (~niemand@98.4.96.130)
2020-09-19 08:07:07 <edwardk> er using lowercase Pi's there
2020-09-19 08:07:20 <dansho> cant figure out this overlapping problem, its ok with the first OVERLAPS (Bar) but error only on the second (Baz) https://hastebin.com/azojuvehes.hs
2020-09-19 08:07:25 × ericsagnes quits (~ericsagne@2405:6580:0:5100:c421:5063:beb8:cd39) (Ping timeout: 272 seconds)
2020-09-19 08:07:26 <dansho> neither Bar nor Baz are Distributions
2020-09-19 08:07:39 <edwardk> man i forgot how much of a PITA template-haskell is to write
2020-09-19 08:07:40 <siraben> Oh, two levels of Pi, I missed that
2020-09-19 08:07:45 <edwardk> its gorgeous once it is written
2020-09-19 08:07:50 <edwardk> but its frustrating to write
2020-09-19 08:08:01 <edwardk> well, not very gorgeous once written, because then someone has to maintain it
2020-09-19 08:08:09 <siraben> Yay it works
2020-09-19 08:08:13 <edwardk> ok, so its a shit show all around, but its still convenient
2020-09-19 08:08:13 <siraben> hasType' (lam "A" (lam "a" (Var "a"))) (pi "A" Star (pi "_" (Var "A") (Var "A")))
2020-09-19 08:08:24 <siraben> Ok so I think the typechecking is correct here then
2020-09-19 08:08:24 <edwardk> yay!
2020-09-19 08:08:32 <siraben> I get, Just (Right ())
2020-09-19 08:08:36 <siraben> it's just right.
2020-09-19 08:08:38 <edwardk> =)
2020-09-19 08:08:59 × lucid_0x80 quits (~lucid_0x8@188.253.237.250) (Remote host closed the connection)
2020-09-19 08:09:07 <siraben> And that's why we want implicit args, heh
2020-09-19 08:09:16 <dansho> like why would ghc even consider the Distribution instance if the type is not an instance?
2020-09-19 08:09:19 → lucid_0x80 joins (~lucid_0x8@188.253.237.250)
2020-09-19 08:09:27 <edwardk> i'm writing more unsafeCoerce's per line right now than I have in years. this is obviously going to work first time, right?
2020-09-19 08:09:33 → gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-19 08:09:42 <siraben> Why are you writing unsafeCoerce?
2020-09-19 08:10:02 <phadej> because edward is smarter than GHC ;)
2020-09-19 08:10:04 <edwardk> https://github.com/ekmett/haskell/blob/master/types/src/Data/Type/Internal.hs
2020-09-19 08:10:34 × rekahsoft quits (~rekahsoft@CPE0008a20f982f-CM64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 260 seconds)
2020-09-19 08:10:48 → dmr0x80 joins (~drm@188.253.237.250)
2020-09-19 08:11:09 <edwardk> that code makes Int, Char usable as a kind and Type,Nat,Symbol usable as terms, and provides one general form of singleton lifting story that is O(1) rather than O(n) like in the singletons library
2020-09-19 08:11:23 <edwardk> but it does so by using evil
2020-09-19 08:11:31 <edwardk> and then unsafeCoercing that evil to make it more evil
2020-09-19 08:12:02 <edwardk> so since the code towards the bottom is super formulaic i want to let template haskell generate it all for the user
2020-09-19 08:13:50 → lateef joins (~lateef@cpe-174-109-67-227.nc.res.rr.com)
2020-09-19 08:14:12 × gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 265 seconds)
2020-09-19 08:14:21 × dmr0x80 quits (~drm@188.253.237.250) (Client Quit)
2020-09-19 08:15:58 <edwardk> the code there can be pretty hard to follow because you need to know what cheats it uses
2020-09-19 08:16:17 → jneira_ joins (~jneira@80.30.101.206)
2020-09-19 08:16:53 <edwardk> newtype Sing (a :: k) = UnsafeSing { fromSing :: k } -- is the first weird to read bit
2020-09-19 08:17:43 <edwardk> it takes a phantom type argument a of kind k, then uses k at the term level as well. So you might have UnsafeSing True :: Sing 'True
2020-09-19 08:18:05 <edwardk> of course its just a phantom so nothing overtly keeps you from saying UnsafeSing False :: Sing 'True
2020-09-19 08:18:09 <edwardk> that is what the rest is for
2020-09-19 08:19:02 <edwardk> the goal is to use Sing (a :: k) as a way to represent terms of type k as a type, with each term getting a different type
2020-09-19 08:19:08 <siraben> I see
2020-09-19 08:19:19 <siraben> I mostly use dependent types for theorem proving, haven't had a use for them in Haskell yet
2020-09-19 08:19:25 <edwardk> the direct way of doing this would be to do this once for each type
2020-09-19 08:19:35 <edwardk> e.g.
2020-09-19 08:19:41 → ericsagnes joins (~ericsagne@2405:6580:0:5100:64a7:3952:c5b0:2946)
2020-09-19 08:19:59 <edwardk> data Nat = Z | S Nat; data SNat (n :: Nat); SZ :: SNat 'Z; SS :: SNat n -> SNat ('S n)
2020-09-19 08:20:12 <edwardk> SNat n and Sing n play the same role here
2020-09-19 08:20:31 → bahamas joins (~lucian@unaffiliated/bahamas)
2020-09-19 08:20:37 × jneira_ quits (~jneira@80.30.101.206) (Ping timeout: 246 seconds)
2020-09-19 08:20:44 <edwardk> i emulate SNat n off of patterns and GADTs and lots of unsafeCoerce below
2020-09-19 08:21:17 → johtso joins (uid563@gateway/web/irccloud.com/x-ycqdrdpxyawcvjxk)
2020-09-19 08:21:21 × lucid_0x80 quits (~lucid_0x8@188.253.237.250) (Remote host closed the connection)
2020-09-19 08:21:37 <siraben> Weird that lifting singletons takes O(n), didn't know that was the case
2020-09-19 08:21:41 → lucid_0x80 joins (~lucid_0x8@188.253.237.250)
2020-09-19 08:21:42 <siraben> In the singletons library
2020-09-19 08:21:52 → jneira_ joins (~jneira@80.30.101.206)
2020-09-19 08:22:31 <edwardk> well its O(1) for each part you touch, but there is a translation cost, because you have to put on and take off the conversions eleemnt by element in say a [a] reflected to a singleton list
2020-09-19 08:23:13 <edwardk> but my goal was to be able to get a singleton Int represented as a machine Int
2020-09-19 08:23:21 <edwardk> rather than some peano monstrosity
2020-09-19 08:23:30 <edwardk> and my singleton list internally to be a list
2020-09-19 08:23:34 <siraben> Since GHC doesn't know about dependent types, how can it perform erasure?
2020-09-19 08:23:45 → Agiza joins (2eef7ad3@larka.olf.sgsnet.se)
2020-09-19 08:24:27 <edwardk> types are still erased
2020-09-19 08:24:48 <Agiza> Hi! Can someone help me with a simple function? I just started learning and can't understand why one function won't work
2020-09-19 08:25:29 × Agiza quits (2eef7ad3@larka.olf.sgsnet.se) (Remote host closed the connection)
2020-09-19 08:25:55 <siraben> oh they left lol
2020-09-19 08:25:59 → Agiza joins (2eef7ad3@larka.olf.sgsnet.se)
2020-09-19 08:26:20 <siraben> Agiza: just ask, don't ask to ask
←Prev  Next→
Page 1 .. 64 65 66 67 68 69 70 71 72 73 74 .. 5022

All times are in UTC.