Newest at the top
| 2025-01-14 18:19:27 +0100 | <kuribas> | haskellbridge: "forall a. a -> a" has term "* -> *", but the first argument is implicit, so inferred by the compiler. |
| 2025-01-14 18:17:24 +0100 | <kuribas> | Which is a Pi type. |
| 2025-01-14 18:17:06 +0100 | <kuribas> | AFAIK "forall a.A" is sugar for "{0 a} -> A". |
| 2025-01-14 18:16:40 +0100 | <kuribas> | haskellbridge: but they are in idris2 |
| 2025-01-14 18:11:49 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-01-14 18:11:48 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 18:05:16 +0100 | dmwit | (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed) |
| 2025-01-14 17:57:36 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2025-01-14 17:56:58 +0100 | <dolio> | Since Π is not the only quantifier when you start getting into such things. |
| 2025-01-14 17:56:08 +0100 | <dolio> | There are some papers on making lambda and pi the same. But they seem misguided to me. |
| 2025-01-14 17:50:44 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-14 17:49:06 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) jespada |
| 2025-01-14 17:43:54 +0100 | EvanR | (~EvanR@user/evanr) EvanR |
| 2025-01-14 17:43:34 +0100 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2025-01-14 17:41:53 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-14 17:37:30 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:36:48 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-01-14 17:35:41 +0100 | <haskellbridge> | <Bowuigi> Instead, combinators should be defined in the usual way but at the type level, using type level lambdas. To get arrows and forall you just add them as combinators, same for pairs, sums, pi types, sigma types, propositional equality types, constraints (the arrow is a "Constraint -> * -> *" operator), etc |
| 2025-01-14 17:34:22 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 252 seconds) |
| 2025-01-14 17:30:32 +0100 | <haskellbridge> | <Bowuigi> The type level combinator system ypu proposed simply wouldn't work. Lemme show you why: Suppose we want to know the type that "I I" expands to. Unfolding everything, using the definition you gave for I ("forall a. a -> a") leaves you with "(forall a. a -> a) (forall a. a -> a)". This term is not well kinded, as you are trying to apply a type of term * to another of term * |
| 2025-01-14 17:28:05 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 17:27:50 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-01-14 17:27:47 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:27:20 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-01-14 17:22:50 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:22:37 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:21:34 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-01-14 17:21:14 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2025-01-14 17:20:45 +0100 | <haskellbridge> | <Bowuigi> The note on erasure is correct tho IIRC |
| 2025-01-14 17:20:26 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:20:16 +0100 | <haskellbridge> | <Bowuigi> kuribas re:dependent-type-forall even from a dependent type viewpoint, foralls are not lambdas, but it unifies type lambdas and term lambdas (both term level constructs) into one |
| 2025-01-14 17:19:46 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-14 17:15:12 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-14 17:10:07 +0100 | Digit | (~user@user/digit) Digit |
| 2025-01-14 17:04:34 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 17:04:16 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:00:34 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 16:59:24 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-14 16:56:40 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 16:52:41 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-14 16:44:32 +0100 | inedia | (~irc@2600:3c00:e000:287::1) dove |
| 2025-01-14 16:41:43 +0100 | <merijn> | I don't really go to more frequent things than NL-FP :p |
| 2025-01-14 16:41:06 +0100 | Digit | (~user@user/digit) (Remote host closed the connection) |
| 2025-01-14 16:41:03 +0100 | <__monty__> | Either way, my info dates back 7-ish years. So I don't have current info. |
| 2025-01-14 16:40:11 +0100 | <__monty__> | [exa]: I think the Leuven HUG kinda stopped meeting? And if people were coming from Gent to Leuven I kinda feel like the answer is no, at least for Flanders. I don't know about the NeLux part of that though, Merijn and tomsmeding might know for NL? |
| 2025-01-14 16:38:14 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-14 16:36:26 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2025-01-14 16:35:58 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-14 16:35:10 +0100 | turlando | (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 2025-01-14 16:34:24 +0100 | <haskellbridge> | <Morj> Coq can extract programs to multiple languages, including ocaml and haskell. Coq itself is writte in ocaml |