Newest at the top
| 2025-01-16 14:44:10 +0100 | <__monty__> | That changes nothing about whether or not the type is inhabited though? |
| 2025-01-16 14:42:48 +0100 | <geekosaur> | because if it's not lazy then it is necessarily fully evaluated already and any nbottom would have already been triggered |
| 2025-01-16 14:36:39 +0100 | <__monty__> | I don't see why not? |
| 2025-01-16 14:35:07 +0100 | m5zs7k | (aquares@web10.mydevil.net) m5zs7k |
| 2025-01-16 14:34:09 +0100 | Digitteknohippie | (~user@user/digit) (Ping timeout: 248 seconds) |
| 2025-01-16 14:33:00 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-16 14:29:32 +0100 | <kuribas> | If it's not lazy, can it be bottom? |
| 2025-01-16 14:27:52 +0100 | <__monty__> | Except for bottom, yes. |
| 2025-01-16 14:27:38 +0100 | <kuribas> | An uninhabited newtype? |
| 2025-01-16 14:27:14 +0100 | <kuribas> | What does that even mean? |
| 2025-01-16 14:26:59 +0100 | <dminuoso> | But cute trick, did not know you could do that. |
| 2025-01-16 14:26:41 +0100 | <dminuoso> | Guess that works too. |
| 2025-01-16 14:26:36 +0100 | <yahb2> | <interactive>:23:1: error: [GHC-39999] ; • No instance for ‘Show Bar’ ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; • In a stmt of an interactive GHCi command: ; Yahb2D... |
| 2025-01-16 14:26:36 +0100 | <dminuoso> | % undefined :: Bar |
| 2025-01-16 14:26:15 +0100 | <yahb2> | <no output> |
| 2025-01-16 14:26:15 +0100 | <Leary> | % newtype Bar = Bar Bar |
| 2025-01-16 14:26:12 +0100 | <dminuoso> | Oh, right. Thanks |
| 2025-01-16 14:26:01 +0100 | <__monty__> | (inhabited) |
| 2025-01-16 14:24:50 +0100 | <dminuoso> | Now it would be interesting if we could conjure `newtype Bar` equivalently |
| 2025-01-16 14:24:31 +0100 | <dminuoso> | Here you have a type `Foo` inhabitated only by bottom. |
| 2025-01-16 14:24:22 +0100 | <yahb2> | <no output> |
| 2025-01-16 14:24:22 +0100 | <dminuoso> | % data Foo |
| 2025-01-16 14:24:19 +0100 | <dminuoso> | And if "inhabitated by bottom" only came to mind |
| 2025-01-16 14:23:41 +0100 | <dminuoso> | Since even `Type` is inhabitated (by bottom), you cannot even differentiate in terms of "is it habitated" |
| 2025-01-16 14:23:05 +0100 | <dminuoso> | That's really the point of it. |
| 2025-01-16 14:23:02 +0100 | <dminuoso> | Well, the distinction is lost with TypeInType. |
| 2025-01-16 14:22:44 +0100 | <kuribas> | I suppose. '*' or 'Type' is the "kind" Type, while other kinds are also types, but not the "kind" type.. |
| 2025-01-16 14:22:42 +0100 | <dminuoso> | type Type = TYPE LiftedRep |
| 2025-01-16 14:22:38 +0100 | <dminuoso> | One particular note here: |
| 2025-01-16 14:22:01 +0100 | <dminuoso> | kuribas: Does that answer your question? |
| 2025-01-16 14:21:28 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cb37:dc44:25ad:be87) |
| 2025-01-16 14:21:25 +0100 | <yahb2> | <no output> |
| 2025-01-16 14:21:25 +0100 | <dminuoso> | % a = undefined :: Type |
| 2025-01-16 14:21:22 +0100 | <yahb2> | <no output> |
| 2025-01-16 14:21:22 +0100 | <dminuoso> | % import Data.Kind |
| 2025-01-16 14:21:20 +0100 | m5zs7k | (aquares@web10.mydevil.net) (Ping timeout: 265 seconds) |
| 2025-01-16 14:20:39 +0100 | <yahb2> | <interactive>:7:14: error: [GHC-76037] ; Not in scope: type constructor or class ‘Type’ |
| 2025-01-16 14:20:39 +0100 | <dminuoso> | % undefined :: Type |
| 2025-01-16 14:20:32 +0100 | <yahb2> | <interactive>:5:14: warning: [GHC-39567] [-Wstar-is-type] ; Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’ ; relies on the StarIsType extension, which will become ; depreca... |
| 2025-01-16 14:20:31 +0100 | <dminuoso> | % undefined :: * |
| 2025-01-16 14:20:13 +0100 | <dminuoso> | * and Int are *distinct* types. |
| 2025-01-16 14:20:07 +0100 | <dminuoso> | What do you mean by distinction? |
| 2025-01-16 14:19:49 +0100 | <kuribas> | Then there is no distinction between types '*' and types with other kinds, even though '*' is named 'Type'? |
| 2025-01-16 14:19:07 +0100 | <kuribas> | right. |
| 2025-01-16 14:18:20 +0100 | <dminuoso> | Types of * are inhabitable, but not necessarily habitated. |
| 2025-01-16 14:18:10 +0100 | <dminuoso> | kuribas: Types of type * -> * are uninhabitable. |
| 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. |