Logs: liberachat/#haskell
| 2021-06-02 21:54:51 | <boxscape> | what's the difference between uninhabitable and uninhabited? |
| 2021-06-02 21:54:55 | × | o1lo01ol1o quits (~o1lo01ol1@c-73-10-81-85.hsd1.nj.comcast.net) (Ping timeout: 245 seconds) |
| 2021-06-02 21:55:10 | <djb2021> | ah ok, and Light could be called a (parametric) type constructor? |
| 2021-06-02 21:55:25 | <dminuoso> | boxscape: I guess there is none, mmm |
| 2021-06-02 21:55:35 | <hpc> | djb2021: yep, it's like how Just is a data constructor |
| 2021-06-02 21:56:01 | <dminuoso> | djb2021: as a point of interest, one might wonder what makes a "constructor a constructor" - my mind model is, its something you can pattern match on. |
| 2021-06-02 21:56:01 | <djb2021> | ah ok |
| 2021-06-02 21:56:11 | <hpc> | djb2021: there's another good example if you've gotten into type classes |
| 2021-06-02 21:56:14 | <hpc> | % :k Functor |
| 2021-06-02 21:56:14 | <yahb> | hpc: (Type -> Type) -> Constraint |
| 2021-06-02 21:56:24 | <dminuoso> | djb2021: a data constructor you can pattern match with case-of, a type constructor you can pattern match with a type family (or a typeclass instance) |
| 2021-06-02 21:56:25 | <nitrix> | Yeah, if you can construct it, you can deconstruct it. |
| 2021-06-02 21:56:34 | <hpc> | Functor takes a parameter that's (Type -> Type) - Maybe, for example |
| 2021-06-02 21:56:45 | <hpc> | and produces a Constraint, which is the kind of things that go on the left of => |
| 2021-06-02 21:56:48 | → | river joins (~river@tilde.team/user/river) |
| 2021-06-02 21:56:55 | <dminuoso> | Though, Functor opens another can of worms |
| 2021-06-02 21:56:57 | <dminuoso> | and requires ConstraintKinds |
| 2021-06-02 21:57:02 | <dminuoso> | To talk about here |
| 2021-06-02 21:57:06 | <hpc> | true |
| 2021-06-02 21:57:13 | <djb2021> | very interesting - i had a completely different model -- something that constructs a thing such as data or now types.... |
| 2021-06-02 21:57:40 | <dminuoso> | djb2021: Inded, `Maybe Int` creates a new type (that has no name other than `Maybe Int` itself) |
| 2021-06-02 21:57:51 | <dminuoso> | djb2021: Here's a very simple rule by the way: |
| 2021-06-02 21:58:10 | <dminuoso> | A type can only be inhabited, if its type is Type |
| 2021-06-02 21:58:18 | <dminuoso> | To check: |
| 2021-06-02 21:58:21 | <dminuoso> | % :k Int |
| 2021-06-02 21:58:21 | <yahb> | dminuoso: Type |
| 2021-06-02 21:58:28 | <dminuoso> | So `Int` is inhabited. |
| 2021-06-02 21:58:32 | <dminuoso> | We can ask GHC to verify: |
| 2021-06-02 21:58:38 | <dminuoso> | % f :: Int; f = undefined |
| 2021-06-02 21:58:38 | <yahb> | dminuoso: |
| 2021-06-02 21:58:53 | <dminuoso> | Type checks, we have a value of type Int. So its inhabited. |
| 2021-06-02 21:58:59 | <dminuoso> | f :: Maybe; f = undefined |
| 2021-06-02 21:59:02 | <dminuoso> | % f :: Maybe; f = undefined |
| 2021-06-02 21:59:02 | <yahb> | dminuoso: ; <interactive>:77:6: error:; * Expecting one more argument to `Maybe'; Expected a type, but `Maybe' has kind `Type -> Type'; * In the type signature: f :: Maybe |
| 2021-06-02 21:59:05 | <dminuoso> | Fails to type check! |
| 2021-06-02 21:59:10 | <dminuoso> | % :k Maybe |
| 2021-06-02 21:59:10 | <yahb> | dminuoso: Type -> Type |
| 2021-06-02 21:59:23 | <hpc> | % f :: 'Red; f = undefined |
| 2021-06-02 21:59:24 | <yahb> | hpc: ; <interactive>:79:6: error:; * Expected a type, but 'Red has kind `Color'; * In the type signature: f :: 'Red |
| 2021-06-02 21:59:39 | <dminuoso> | The diagnostic is poor |
| 2021-06-02 21:59:49 | <dminuoso> | when GHC says "Expected a type", it really means "a type of kind/type Type" |
| 2021-06-02 22:00:47 | <djb2021> | is there a function to transcript this conversation? |
| 2021-06-02 22:00:56 | <dminuoso> | djb2021: Check the topic |
| 2021-06-02 22:01:00 | <djb2021> | i want to read it tomorrow again |
| 2021-06-02 22:01:06 | <dminuoso> | We provide full channel logging |
| 2021-06-02 22:01:12 | <dminuoso> | /topic |
| 2021-06-02 22:01:37 | <dminuoso> | djb2021: in hpc's example, because the type of 'Red is Color (i.e. 'Red :: Color -- note that both left hand and right hand side are types), there exists no values of type 'Red, not even undefined. |
| 2021-06-02 22:01:46 | <dminuoso> | (Because again, the type of 'Red is not Type) |
| 2021-06-02 22:01:50 | <nitrix> | dminuoso, Most IRC clients let you escape / with another /, so //topic should work, or you can also do /say /topic which I think is in the RFC. |
| 2021-06-02 22:01:57 | <dminuoso> | /foo |
| 2021-06-02 22:02:03 | <dminuoso> | nitrix: Ah I was always curious about the syntax :) |
| 2021-06-02 22:02:07 | <nitrix> | :) |
| 2021-06-02 22:02:26 | <boxscape> | djb2021 these are the logs for today https://ircbrowse.tomsmeding.com/day/lchaskell/2021/06/02 |
| 2021-06-02 22:02:39 | <hpc> | one final detail is unboxing |
| 2021-06-02 22:02:40 | <dminuoso> | djb2021: The main usefulness of this DataKinds, is that we can pattern match on these lifted types *similarly* to how we can pattern match on nullary sum types in the value level |
| 2021-06-02 22:02:53 | <dminuoso> | So you could write something like |
| 2021-06-02 22:02:57 | <hpc> | which essentially is for values that don't have all the thunk wrapping around them |
| 2021-06-02 22:03:03 | <hpc> | % :t 5# |
| 2021-06-02 22:03:03 | <yahb> | hpc: Int# |
| 2021-06-02 22:03:07 | <hpc> | % :k Int# |
| 2021-06-02 22:03:07 | <yahb> | hpc: TYPE 'GHC.Exts.IntRep |
| 2021-06-02 22:03:09 | <djb2021> | boxscape: thank you very much |
| 2021-06-02 22:03:22 | <hpc> | you don't really get into that unless you're doing FFI or really heavy optimization |
| 2021-06-02 22:03:32 | <hpc> | but it's useful to know it's there |
| 2021-06-02 22:04:46 | <hpc> | the # there is just part of the identifier name, and used by convention to mark unboxed stuff |
| 2021-06-02 22:05:01 | <hpc> | so like you don't get Light# automagically or anything |
| 2021-06-02 22:05:17 | <dminuoso> | % type family Value n :: Nat where Value 'Red = 10; Value 'Green = 20 |
| 2021-06-02 22:05:17 | <yahb> | dminuoso: |
| 2021-06-02 22:05:35 | <dminuoso> | djb2021: ^- here. This is a type level equivalent of `\f -> case f of Red -> 10; Green -> 20` |
| 2021-06-02 22:05:45 | <dminuoso> | (yes, we can have numbers on the type level too!) |
| 2021-06-02 22:05:54 | <hpc> | % :k Value |
| 2021-06-02 22:05:54 | <yahb> | hpc: Color -> Nat |
| 2021-06-02 22:06:10 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 245 seconds) |
| 2021-06-02 22:06:14 | → | ddellacosta joins (~ddellacos@86.106.121.17) |
| 2021-06-02 22:06:43 | <dminuoso> | djb2021: So you see, there's this deep rabbit hole that opens up when you realize this type system lets you pattern match on types, express computations, etc.. |
| 2021-06-02 22:06:50 | × | unyu quits (~pyon@user/pyon) (Ping timeout: 252 seconds) |
| 2021-06-02 22:06:53 | <dminuoso> | Next up we have type level lists too.. |
| 2021-06-02 22:07:00 | × | dhil quits (~dhil@195.213.192.85) (Ping timeout: 245 seconds) |
| 2021-06-02 22:07:21 | × | davidnutting quits (~nuttingd@75.164.99.232) (Quit: WeeChat 3.1) |
| 2021-06-02 22:07:38 | → | davidnutting joins (~nuttingd@75.164.99.232) |
| 2021-06-02 22:07:42 | <dminuoso> | % kind! (Value 'Red) |
| 2021-06-02 22:07:42 | <yahb> | dminuoso: ; <interactive>:100:1: error:; * Variable not in scope: kind :: Array i0 e; * Perhaps you meant one of these: `find' (imported from Data.List), `BSL.find' (imported from Data.ByteString.Lazy), `BS.find' (imported from Data.ByteString); <interactive>:100:8: error: Data constructor not in scope: Value :: Name -> i0 |
| 2021-06-02 22:07:50 | <dminuoso> | % :kind! (Value 'Red) |
| 2021-06-02 22:07:50 | <yahb> | dminuoso: Nat; = 10 |
| 2021-06-02 22:07:54 | <dminuoso> | % :kind! (Value 'Green) |
| 2021-06-02 22:07:54 | <yahb> | dminuoso: Nat; = 20 |
| 2021-06-02 22:08:21 | <djb2021> | wow, currently this blows my mind - but i got a few things the equivalence with match case is clear. |
| 2021-06-02 22:09:38 | <dminuoso> | % :set -XPolyKinds |
| 2021-06-02 22:09:38 | <yahb> | dminuoso: |
| 2021-06-02 22:09:42 | <dminuoso> | % newtype Tagged s b = Tagged b |
| 2021-06-02 22:09:42 | <yahb> | dminuoso: |
| 2021-06-02 22:09:59 | <djb2021> | the "family" in the definition confuses me a little bit - i never used this before |
| 2021-06-02 22:10:09 | <dminuoso> | djb2021: "type family" is just a type level function, nothing more |
| 2021-06-02 22:10:35 | <dminuoso> | well, there's some differences, but you can think of them as type level functions |
| 2021-06-02 22:10:38 | <dminuoso> | type family is just the name for it |
| 2021-06-02 22:10:42 | <hpc> | % class LowerColor (c :: Color) where color :: Color; instance LowerColor Red where color = Red; instanceLowerColor Green where color = Green |
| 2021-06-02 22:10:42 | <yahb> | hpc: ; <interactive>:105:53: error: parse error on input `instance' |
| 2021-06-02 22:10:55 | × | Ariakenom quits (~Ariakenom@2001:9b1:efb:fc00:8504:3672:14f4:b190) (Quit: Leaving) |
| 2021-06-02 22:10:58 | <hpc> | % class LowerColor (c :: Color) where color :: Color |
| 2021-06-02 22:10:59 | <yahb> | hpc: ; <interactive>:106:37: error:; * Could not deduce (LowerColor c0); from the context: LowerColor c; bound by the type signature for:; color :: forall (c :: Color). LowerColor c => Color; at <interactive>:106:37-50; The type variable `c0' is ambiguous; * In the ambiguity check for `color'; To defer the ambiguity check to use sites, enable AllowAmb |
All times are in UTC.