Newest at the top
2024-05-21 11:07:46 +0200 | <ski> | it's a mess |
2024-05-21 11:06:14 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
2024-05-21 11:06:11 +0200 | <tomsmeding> | if you squint on fromInteger you can maybe make Num work, but that's as far as you get |
2024-05-21 11:05:41 +0200 | <tomsmeding> | there's no sensible way to make arrays an instance of the numeric hierarchy |
2024-05-21 11:05:32 +0200 | <tomsmeding> | I guess my actual X question is: why are all the numeric classes specifically for single scalars |
2024-05-21 11:05:20 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds) |
2024-05-21 11:05:04 +0200 | <ncf> | well i guess not decidably so |
2024-05-21 11:05:02 +0200 | <tomsmeding> | you have a point |
2024-05-21 11:04:45 +0200 | <ncf> | the reals are ordered aren't they |
2024-05-21 11:04:07 +0200 | <tomsmeding> | why is Ord a superclass of Real? |
2024-05-21 10:57:59 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
2024-05-21 10:54:08 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds) |
2024-05-21 10:49:59 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
2024-05-21 10:48:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
2024-05-21 10:47:04 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:6584:33d2:35a2:fd74) |
2024-05-21 10:46:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
2024-05-21 10:43:13 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
2024-05-21 10:42:30 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
2024-05-21 10:37:59 +0200 | <ski> | .. which i guess is another reason i've semi-recently been interested in grokking ordered logic (also for its own sake, e.g. for use as a logic programming language, or a logical framework) |
2024-05-21 10:36:59 +0200 | <ski> | the type system for this requires keeping track of an *ordered* context/environment of variable typings .. |
2024-05-21 10:34:22 +0200 | <ski> | and i'm not too sure how more generally useful it would be .. but it seems like an interesting idea to explore, regardless, to see how far one can push it, how much it can make sense, and perhaps how much can be incorporated in such a system |
2024-05-21 10:33:26 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-05-21 10:33:23 +0200 | <ski> | .. it's a bit weird and unusual to think in these terms |
2024-05-21 10:33:04 +0200 | ft | (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving) |
2024-05-21 10:32:46 +0200 | <vladl> | ah yes that makes sense now |
2024-05-21 10:30:34 +0200 | <ski> | note that, in the `Cons' case of `concat', because `l1' is plural, in the first argument of `append' (whose domain is a (lifted) product, not a composition), `l1' refers to the first list (which is pointed out by the `(||)', in the pattern). wihle in the second argument of `append', `l1' refers to all the other lists, living under the `l0' list structure |
2024-05-21 10:29:48 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
2024-05-21 10:28:57 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) (Ping timeout: 255 seconds) |
2024-05-21 10:28:29 +0200 | <ski> | the `(||)' in the `Cons' case of `append' basically indicates the place of the element (the "hole", since elements are not explicitly mentioned in these operations) |
2024-05-21 10:27:32 +0200 | <ski> | (note that `f . g -> h' here curries as `f -> g -> h' (and `Identity -> h' as `h'). `(f,g) -> h' does not curry (and nor does `() -> h')) |
2024-05-21 10:26:22 +0200 | <ski> | concat (| Cons ((||),l0),l1 |) = append (l1,concat (| l0,l1 |)) |
2024-05-21 10:26:03 +0200 | <ski> | concat (| Nil ( ),l1 |) = Nil ( ) |
2024-05-21 10:25:08 +0200 | <ski> | concat :: List . List -> List |
2024-05-21 10:25:00 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2024-05-21 10:24:54 +0200 | <ski> | and |
2024-05-21 10:24:52 +0200 | <ski> | append (Cons ((||),l0),l1) = Cons ((||),append (l0,l1)) |
2024-05-21 10:24:33 +0200 | <ski> | append (Nil ( ),l1) = l1 |
2024-05-21 10:24:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-05-21 10:23:45 +0200 | <ski> | append :: (List,List) -> List |
2024-05-21 10:23:28 +0200 | <ski> | and then you can do |
2024-05-21 10:23:17 +0200 | <ski> | Cons :: (Identity,List) -> List |
2024-05-21 10:22:58 +0200 | <ski> | Nil :: ( ) -> List |
2024-05-21 10:22:39 +0200 | <ski> | where |
2024-05-21 10:22:29 +0200 | <ski> | data List :: * -> * |
2024-05-21 10:22:22 +0200 | <ski> | something like |
2024-05-21 10:17:35 +0200 | __monty__ | (~toonn@user/toonn) |
2024-05-21 10:16:27 +0200 | danse-nr3 | (~danse-nr3@151.35.171.208) |
2024-05-21 10:12:26 +0200 | <ski> | or defining the operation |
2024-05-21 10:12:12 +0200 | <ski> | yes |
2024-05-21 10:11:51 +0200 | <ski> | (well, preferably it'd work for `f :: k0 -> k1' ..) |