Newest at the top
| 2025-01-16 14:17:58 +0100 | <lambdabot> | * -> * |
| 2025-01-16 14:17:57 +0100 | <kuribas> | :k Maybe |
| 2025-01-16 14:17:56 +0100 | AlexZenon | (~alzenon@178.34.163.23) |
| 2025-01-16 14:17:49 +0100 | <kuribas> | No, "Maybe" is not inhabited. |
| 2025-01-16 14:17:34 +0100 | <kuribas> | So there is a difference betwee "Types" and "Type"? |
| 2025-01-16 14:17:32 +0100 | <dminuoso> | In fact, inhabitation and *inhabitability* are qualities of all types. |
| 2025-01-16 14:17:15 +0100 | <dminuoso> | Nope? |
| 2025-01-16 14:17:06 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2025-01-16 14:17:05 +0100 | <kuribas> | Aren't types supposed to be inhabited? |
| 2025-01-16 14:16:41 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-01-16 14:16:31 +0100 | AlexNoo | (~AlexNoo@178.34.163.23) |
| 2025-01-16 14:16:10 +0100 | <dminuoso> | kuribas: Yes, TypeInType is (in effect) on by default and cannot be turned off. |
| 2025-01-16 14:14:46 +0100 | Digit | (~user@user/digit) (Ping timeout: 252 seconds) |
| 2025-01-16 14:13:53 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cb37:dc44:25ad:be87) (Ping timeout: 248 seconds) |
| 2025-01-16 14:13:30 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2025-01-16 14:12:28 +0100 | <lambdabot> | * |
| 2025-01-16 14:12:27 +0100 | <kuribas> | :k * -> * |
| 2025-01-16 14:12:11 +0100 | <kuribas> | Is '* -> *' considered a type? |
| 2025-01-16 14:06:43 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cb37:dc44:25ad:be87) |
| 2025-01-16 14:05:54 +0100 | rvalue- | rvalue |
| 2025-01-16 14:04:27 +0100 | PHO` | (~pho@akari.cielonegro.org) PHO` |
| 2025-01-16 14:03:46 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d12f:67f5:c2b0:5368) (Ping timeout: 248 seconds) |
| 2025-01-16 14:00:21 +0100 | PHO` | (~pho@akari.cielonegro.org) (Quit: SIGTERM received; exit) |
| 2025-01-16 14:00:12 +0100 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 264 seconds) |
| 2025-01-16 13:59:58 +0100 | housemate | (~housemate@146.70.66.228) housemate |
| 2025-01-16 13:59:44 +0100 | Guest38 | (~Guest38@2a02:a03f:c0fd:e500:6c68:1cd6:8c4:155f) (Client Quit) |
| 2025-01-16 13:58:43 +0100 | Guest38 | (~Guest38@2a02:a03f:c0fd:e500:6c68:1cd6:8c4:155f) |
| 2025-01-16 13:58:04 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-01-16 13:57:53 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 2025-01-16 13:57:47 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2025-01-16 13:57:13 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-01-16 13:57:12 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d12f:67f5:c2b0:5368) |
| 2025-01-16 13:55:06 +0100 | xff0x | (~xff0x@2405:6580:b080:900:7761:255c:77e5:46e1) (Quit: xff0x) |
| 2025-01-16 13:50:32 +0100 | <kuribas> | tomsmeding: My goal is to have a verified implementation of https://www.cl.cam.ac.uk/~nk480/bidir.pdf, then add higher kinded types, type classes, data kinds and type families. |
| 2025-01-16 13:49:03 +0100 | <kuribas> | tomsmeding: a verified checker. |
| 2025-01-16 13:48:30 +0100 | <kuribas> | basically "forall (a:k) . t" |
| 2025-01-16 13:47:59 +0100 | <kuribas> | Forall : String -> (k:Kind) -> PolyType l -> PolyType l |
| 2025-01-16 13:47:35 +0100 | <kuribas> | tomsmeding: I've started a type checker in idris. I am using normal substitution for now. |
| 2025-01-16 13:46:31 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-16 13:46:11 +0100 | AlexNoo | (~AlexNoo@178.34.163.23) (Quit: Leaving) |
| 2025-01-16 13:44:50 +0100 | user363627 | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-16 13:42:56 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-16 13:42:09 +0100 | AlexZenon | (~alzenon@178.34.163.23) (Quit: ;-) |
| 2025-01-16 13:40:21 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 248 seconds) |
| 2025-01-16 13:36:20 +0100 | user363627 | (~user@user/user363627) user363627 |
| 2025-01-16 13:35:40 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 13:35:22 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:35:01 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) |
| 2025-01-16 13:34:52 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:32:56 +0100 | ColinRobinson | JuanDaugherty |