Newest at the top
2025-05-07 23:54:19 +0200 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/2b39ca47cb55324cab4eda36c0546ea1fb3d7aca/hs-pkgs… this is an example of native-haskell pattern matching. there is a sharing problem, but I resolved it with exponential object. Not sure I can explain that today. |
2025-05-07 23:54:15 +0200 | <EvanR> | let's let the let example loose |
2025-05-07 23:53:10 +0200 | <tomsmeding> | sure |
2025-05-07 23:53:02 +0200 | <hellwolf> | ah, okay, perhaps let's just leave it here and talk about it another day. I will just show you the "let" example |
2025-05-07 23:52:46 +0200 | <tomsmeding> | it's 23:52 over here |
2025-05-07 23:52:40 +0200 | <tomsmeding> | I'm interested, but not now :') |
2025-05-07 23:52:31 +0200 | <hellwolf> | but bear with me... I haven't had write up, so I am now typing from scratch |
2025-05-07 23:52:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-05-07 23:52:17 +0200 | <hellwolf> | I will get there, there is technique to avoid that; and the lineartype provided scenario is even more interesting to talk about. |
2025-05-07 23:51:50 +0200 | <tomsmeding> | assuming you care about that :) |
2025-05-07 23:51:41 +0200 | <tomsmeding> | an duplication is usually bad for performance |
2025-05-07 23:51:30 +0200 | <hellwolf> | let me show you an example. |
2025-05-07 23:51:14 +0200 | <tomsmeding> | can't represent that diagram without let-binding |
2025-05-07 23:51:05 +0200 | <hellwolf> | And since they are "pure", if such duplication actually happens, it's fine, it's referential transparent. |
2025-05-07 23:51:04 +0200 | <tomsmeding> | but what if I want `let z = x + y in z + z`? |
2025-05-07 23:50:28 +0200 | <hellwolf> | For pure morphisms, everything is just a "diagram". And since I don't implement lambda, there is no "Let" constructor. if you do x + x, diagrams "x" got duplicated and their outputs are sent to (+) morphism. |
2025-05-07 23:49:11 +0200 | <hellwolf> | First of all, all functions (a morphism in the category) in yolc has a "eff" tag, which classifies into either pure, and non-pure. Just like Haskell's IO or the lack of IO as tag. |
2025-05-07 23:47:39 +0200 | <hellwolf> | yea, that's right. There are two scenarios in my case. |
2025-05-07 23:47:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-05-07 23:46:27 +0200 | <tomsmeding> | (IMO sharing is the big design choice when designing an embedded language in haskell) |
2025-05-07 23:46:06 +0200 | <tomsmeding> | i.e. do you have a let-binding construct in your embedded language, and if so, how do you expose that to the user |
2025-05-07 23:45:39 +0200 | <tomsmeding> | how would you have the user represent sharing in their embedded program? |
2025-05-07 23:45:12 +0200 | <tomsmeding> | embedding is much easier :D |
2025-05-07 23:45:03 +0200 | <tomsmeding> | I might be able to finish it if I spend more time on it |
2025-05-07 23:44:56 +0200 | <hellwolf> | I am not versed in to actually building those. Using embedding approach is more because of my limitation. |
2025-05-07 23:44:30 +0200 | <tomsmeding> | at some point I tried to implement a haskell typechecker (well, a very small subset of haskell), without reference to literature because it's more fun that way, and I got stuck at properly handling inference of polymorphic functions |
2025-05-07 23:44:29 +0200 | <hellwolf> | oh, yea, I think I read some of Arnauld's paper. Linear-types rules seems very concise. |
2025-05-07 23:44:20 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
2025-05-07 23:44:06 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2025-05-07 23:43:36 +0200 | <tomsmeding> | *daunted |
2025-05-07 23:43:32 +0200 | <tomsmeding> | I wouldn't be scared from having to implement linearity, whereas I'm still dauted by GADTs |
2025-05-07 23:43:12 +0200 | <tomsmeding> | actually, as advanced type systems go, linear types are not so bad |
2025-05-07 23:43:01 +0200 | <hellwolf> | I can explain, but I might butcher it in IRC format. |
2025-05-07 23:42:52 +0200 | <tomsmeding> | I see |
2025-05-07 23:42:44 +0200 | <hellwolf> | no, but I actually need multiplicity on arrows |
2025-05-07 23:42:34 +0200 | <tomsmeding> | (Futhark is completely unsuitable for what you're trying to do, by the way) |
2025-05-07 23:42:27 +0200 | <hellwolf> | okay, good to know :) |
2025-05-07 23:42:18 +0200 | <tomsmeding> | well, Futhark has uniqueness types :) |
2025-05-07 23:42:05 +0200 | <hellwolf> | tomsmeding: well, I use LinearTypes, so that's that :D |
2025-05-07 23:41:43 +0200 | <hellwolf> | so, it is rather a haskell problem. |
2025-05-07 23:41:38 +0200 | <tomsmeding> | all the ML stuff is embedded in python |
2025-05-07 23:41:29 +0200 | <hellwolf> | true. |
2025-05-07 23:41:27 +0200 | <tomsmeding> | or Python, actually |
2025-05-07 23:41:19 +0200 | <tomsmeding> | embedding in javascript is very fashionable, I think |
2025-05-07 23:41:08 +0200 | <tomsmeding> | is it not fashionable? |
2025-05-07 23:40:50 +0200 | <hellwolf> | logic and "next 700 programming language" suggests embedding language is the way; but rationality not culturally fasionable atm. |
2025-05-07 23:40:48 +0200 | <int-e> | and it feels relevant to trying to sell Haskell :) |
2025-05-07 23:40:30 +0200 | <tomsmeding> | hellwolf: how advanced of a type system do you need? |
2025-05-07 23:40:07 +0200 | <int-e> | tomsmeding: it's a favorite |
2025-05-07 23:40:00 +0200 | <tomsmeding> | int-e: you've quoted that one before :p |