Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 12 13 14 15 16 17 18 19 20 21 22 .. 5022
— 502,152 events total
2020-09-17 06:18:01 → ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex)
2020-09-17 06:18:31 <edwardk> https://github.com/AndrasKovacs/implicit-fun-elaboration/blob/master/fcif/Elaboration.hs#L513 -- here's a version from andras kovacs
2020-09-17 06:19:26 → danvet joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa)
2020-09-17 06:19:30 → mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848)
2020-09-17 06:19:32 → danvet_ joins (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453)
2020-09-17 06:19:33 → mmohammadi9812 joins (~mmohammad@5.116.223.123)
2020-09-17 06:19:44 → hvr joins (~hvr@haskell/developer/hvr)
2020-09-17 06:19:45 × danvet_ quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Client Quit)
2020-09-17 06:20:01 <edwardk> that is in the 'infer' case for app, which delegates to an infer for the function, notice how it has to manufacture a couple of meta variables
2020-09-17 06:20:34 <edwardk> (notice there is a separate 'check' and infer and check bounce back and forth, bidirectional style
2020-09-17 06:20:49 <siraben> Heh, going straight for the IO monad
2020-09-17 06:20:53 <siraben> Right
2020-09-17 06:21:28 <edwardk> yeah andras runs in strict haskell and does evil things for IO
2020-09-17 06:21:43 <edwardk> I use slightly less evil things, but then unsafeInterleaveIO all over the same code =P
2020-09-17 06:22:00 → kori joins (~kori@2804:14c:85a3:9105::1000)
2020-09-17 06:22:00 × kori quits (~kori@2804:14c:85a3:9105::1000) (Changing host)
2020-09-17 06:22:00 → kori joins (~kori@arrowheads/kori)
2020-09-17 06:22:11 <edwardk> i've been basing things pretty closely on his work because he gets some pretty great type inference
2020-09-17 06:22:26 <edwardk> e.g. he can handle the runST $ do ... stuff without any magic rule for $.
2020-09-17 06:22:44 <edwardk> so i more or less grabbed that wholesale
2020-09-17 06:23:59 <siraben> Wow, he has an elaboration-zoo repo as well
2020-09-17 06:24:17 × falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection)
2020-09-17 06:24:18 <edwardk> if you rip out all the exotic Tel, PiTel, LamTel, Rec. stuff out of his type theory he gets a pretty good baseline typechecker (modulo the usual sort of implicit reordering that agda does)
2020-09-17 06:24:33 × dansho quits (~dansho@ip68-108-167-185.lv.lv.cox.net) (Remote host closed the connection)
2020-09-17 06:24:44 → falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a)
2020-09-17 06:24:47 → dansho joins (~dansho@ip68-108-167-185.lv.lv.cox.net)
2020-09-17 06:24:48 <edwardk> We talked quite a bit at ICFP and it served as a good forcing function for me to stop dilly-dallying with other ways to do this, and just raid his toolbox for tricks
2020-09-17 06:25:11 × heatsink quits (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece) (Remote host closed the connection)
2020-09-17 06:25:42 × echoreply quits (~echoreply@unaffiliated/echoreply) (Quit: WeeChat 1.9.1)
2020-09-17 06:25:50 <edwardk> my usecase is a bit weird
2020-09-17 06:26:01 <edwardk> i'm currently trying to do this to build a "logical framework" like LF
2020-09-17 06:26:13 → echoreply joins (~echoreply@unaffiliated/echoreply)
2020-09-17 06:26:15 <edwardk> but with the qtt bits sprinkled on top
2020-09-17 06:26:49 <edwardk> LF is what you get if you take a dependent type theory, lop it off at the knees and stunt its growth.
2020-09-17 06:27:18 → heatsink joins (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece)
2020-09-17 06:27:25 × Cale quits (~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com) (Ping timeout: 246 seconds)
2020-09-17 06:28:10 <edwardk> you remove all the bits that have to do with sigma, maybe cripple pi so you can make types that depend on terms but not use other things, force yourself to only have terms, types and kinds, and no universe tower, don't bother making traditional data types and induction principles and the like.
2020-09-17 06:28:27 × Neuromancer quits (~Neuromanc@unaffiliated/neuromancer) (Ping timeout: 240 seconds)
2020-09-17 06:28:37 <edwardk> which seems like an awful lot of surgery to do
2020-09-17 06:29:03 <edwardk> but once you've butcher the type system in this way, it becomes really easy to reason about HOAS.
2020-09-17 06:30:06 <edwardk> e.g. you can define tm : type; lam : (tm -> tm) -> tm; app : tm -> tm -> tm -- and have a higher order abstract syntax for terms. and you can know that that function from tm -> tm in lam just places the argument somewhere, BECAUSE IT CANT PATTERN MATCH ON IT.
2020-09-17 06:30:14 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 272 seconds)
2020-09-17 06:30:16 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-09-17 06:30:22 <edwardk> so you write your semantics in this logical framework and what have you
2020-09-17 06:31:01 × mmohammadi9812 quits (~mmohammad@5.116.223.123) (Quit: I quit (╯°□°）╯︵ ┻━┻)
2020-09-17 06:31:07 <edwardk> and then reason about meta theorems about what you wrote, and those are simplified by the fact that the language the code manipulating your terms or judging things about your terms was written in is comparatively simple
2020-09-17 06:31:37 <edwardk> i figured i'd share because you started from 'hey i wrote down the denotational semantics of r5rs and ran them'
2020-09-17 06:32:18 × kori quits (~kori@arrowheads/kori) (Quit: WeeChat 2.8)
2020-09-17 06:32:27 <edwardk> normally to work with syntax tree representations you have to go off and fight with debruijn indices/levels or use 'parametric hoas' or use a library like bound or unbound or nominal or name...
2020-09-17 06:32:39 <edwardk> but each of those complicate reasoning about the program that manipulates those terms
2020-09-17 06:32:43 → mmohammadi9812 joins (~mmohammad@5.116.223.123)
2020-09-17 06:32:52 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-09-17 06:33:15 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-17 06:33:25 <siraben> Thanks, that was insightful.
2020-09-17 06:33:26 <edwardk> so the old-school bob harper way to handle that was to build a crippled but still usable type system that was good enough for building up those judgments
2020-09-17 06:33:54 <siraben> Capture-avoiding substitution is a mess, I've recently using de bruijn to implement a linearly typed lambda calculus.
2020-09-17 06:33:57 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection)
2020-09-17 06:34:05 → finkata joins (~dpetrov@83.222.188.39)
2020-09-17 06:34:14 → incognito9999 joins (~incognito@hwsrv-648981.hostwindsdns.com)
2020-09-17 06:34:14 <siraben> Thinking about implementing lambda pi from https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
2020-09-17 06:34:17 → __Joker joins (~Joker@180.151.106.108)
2020-09-17 06:34:31 → josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net)
2020-09-17 06:34:43 <edwardk> i've been playing with ways to extend an LF, because, say, working on a language that has linear types in LF is awful. your binding forms don't match the host LF's binding forms in how they are managed and so all of a sudden you're stuck in debruijn hell... in a crippled type theory
2020-09-17 06:34:44 <siraben> edwardk: do you know if tagless final can be used to implement dependently typed languages?
2020-09-17 06:34:55 × josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Read error: Connection reset by peer)
2020-09-17 06:35:39 <edwardk> but if the lf itself has qtt, then it becomes pretty easy to reason about any language that uses a binding form that has constraints that look like any subsemiring of the ones offered by the host language.
2020-09-17 06:35:50 <edwardk> (there was some work on linear logical frameworks in the 90s)
2020-09-17 06:35:58 <edwardk> the answer is a hard 'sorta'
2020-09-17 06:36:12 <edwardk> so lets use the running example of an LF
2020-09-17 06:36:16 <edwardk> because its on my brain
2020-09-17 06:36:23 <edwardk> here we have 'dependent types' where types can depend on terms
2020-09-17 06:37:12 <edwardk> i wrote some code the other day and posted it to twitter for how to do typed "normalization-by-evaluation"
2020-09-17 06:37:35 <edwardk> https://gist.github.com/ekmett/6c64c3815f9949d067d8f9779e2347ef
2020-09-17 06:38:14 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2020-09-17 06:38:18 <edwardk> if you look at the very bottom of that code id_, k, kid_ are id, const, and const id in the little toy 'untyped except i happen to be borrowing haskell's types' typed language.
2020-09-17 06:38:37 <edwardk> basically Val represents terms crushed down to normal form.
2020-09-17 06:38:44 <edwardk> and expressions allows for you to be sloppier
2020-09-17 06:39:02 → Cale joins (~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com)
2020-09-17 06:39:11 <edwardk> nf takes an expression to a val, which is internally representing something in beta normal form, and then converts the val back to an expr which happens to be in beta normal form
2020-09-17 06:39:37 <edwardk> so what does this have to do with dependently typed languages? this is clearly an untyped language
2020-09-17 06:39:45 <edwardk> well, haskelly-typed
2020-09-17 06:40:09 <edwardk> well, an old paper of conal elliott's (maybe his thesis, i forget) introduced a notion of 'approximately well typed' programs
2020-09-17 06:40:57 <edwardk> which is to say if you run through an LF and rip out all the dependent bits, turning [| Pi x : A. B |]. into [| A |] -> [| A |] ...
2020-09-17 06:41:05 <edwardk> er B
2020-09-17 06:41:21 <edwardk> then you get a non-dependently typed approxmation of the types in the LF
2020-09-17 06:41:48 <edwardk> and termination of unification, etc. in the LF is sort of governed by termination of it for this crippled type
2020-09-17 06:42:11 × ystael quits (~ystael@209.6.50.55) (Ping timeout: 240 seconds)
2020-09-17 06:42:28 × mmohammadi9812 quits (~mmohammad@5.116.223.123) (Quit: I quit (╯°□°）╯︵ ┻━┻)
2020-09-17 06:42:53 <edwardk> so if you were working with something in the LF corner of the lambda cube where you have limited dependent types? then you can use what host language types those types erased to and have an 'approximately well typed' scheme for working with it, implemented finally tagless style
2020-09-17 06:43:33 <edwardk> but the finally-tagless bits? i personally tend to go for heavier tagged deep embeddings because i find they are really frustrating to work with when you want sweeter sugar
2020-09-17 06:43:33 → ystael joins (~ystael@209.6.50.55)
2020-09-17 06:43:50 <edwardk> er they here being finally tagless
2020-09-17 06:43:52 <siraben> That makes sense
2020-09-17 06:44:15 → mmohammadi9812 joins (~mmohammad@5.116.223.123)
2020-09-17 06:44:18 <edwardk> http://www.cse.chalmers.se/~josefs/publications/svenningsson2015combining.pdf is a paper on how to do typed EDSLs that I rather like
2020-09-17 06:44:31 <edwardk> iceland jack posted a link to it the other day on twitter and it reminded me of its existence
2020-09-17 06:44:48 <edwardk> in theory a version of that that is 'approximately well typed' could work for an LF.
2020-09-17 06:45:06 <edwardk> so that gives the 'can i get the types right' answer with a sort of strong maybe.
2020-09-17 06:45:21 × mmohammadi9812 quits (~mmohammad@5.116.223.123) (Client Quit)
2020-09-17 06:46:03 <edwardk> for working with dependent types in general i tend to stick to real syntax trees and libraries like bound.
←Prev  Next→
Page 1 .. 12 13 14 15 16 17 18 19 20 21 22 .. 5022

All times are in UTC.