Newest at the top
| 2024-05-07 17:08:02 +0200 | lg188 | (~lg188@82.18.98.230) (Client Quit) |
| 2024-05-07 17:07:44 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-05-07 17:04:29 +0200 | lg188 | (~lg188@82.18.98.230) (Ping timeout: 252 seconds) |
| 2024-05-07 17:01:52 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-07 17:01:45 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) (Ping timeout: 256 seconds) |
| 2024-05-07 17:01:28 +0200 | img | (~img@user/img) |
| 2024-05-07 17:01:04 +0200 | <lortabac> | having to define everything at top-level is annoying sometimes |
| 2024-05-07 17:00:39 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-07 17:00:34 +0200 | <lortabac> | I didn't know lambdaProlog had it |
| 2024-05-07 17:00:29 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2024-05-07 17:00:26 +0200 | <lortabac> | ski: that's the feature I miss the most in Prolog |
| 2024-05-07 16:59:31 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 16:57:18 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 16:53:23 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-05-07 16:51:08 +0200 | <ski> | (from a programming standpoint, these features are a kind of dynamic scope thing, and can be used for somewhat similar effect you could use dynamic scope for in other languages. it's just that they also have a perfectly sensible logical/declarative semantics here (meaning of implication, and of universal quantification)) |
| 2024-05-07 16:48:23 +0200 | <ski> | e.g. it being assigned a given (object type) (if doing type checking/inference), before traversing into the body of the binder. these local constants and assumptions then automatically vanish after the completion of that, unlike using assert[az]/1,retract/1,gensym/1 in Prolog) |
| 2024-05-07 16:48:17 +0200 | <ski> | (lambdaProlog (and Twelf) also has, from a logic programming standpoint, support for locally assuming extra clauses for predicates, and locally introducing new constants (skolems) of given types. e.g. when you traverse an AST with a bound variable, you locally introduce a new constant, substituting it for the bound variable in the AST, and commonly also locally assume some extra clauses for the constant, |
| 2024-05-07 16:46:17 +0200 | dtman34 | (~dtman34@2601:447:d001:ed50:f596:52e1:73ca:629d) |
| 2024-05-07 16:44:49 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 2024-05-07 16:43:17 +0200 | <ski> | no recursion for functions. you do your computation with predicates/relations, instead) |
| 2024-05-07 16:43:11 +0200 | <ski> | (Twelf also has HOAS support, including matching, in case that wasn't clear from what i said. in Agda, you can't match on functions (apart from calling them), since they're computational .. except that sometimes you do know statically/definitionally something about them. lambdaProlog (and Twelf) doesn't have (full) computational terms, there's only beta- and eta- conversion for functions, there's no `case', |
| 2024-05-07 16:40:41 +0200 | <ski> | it sure is |
| 2024-05-07 16:40:36 +0200 | <Franciman> | lambdaProlog is damn kewl |
| 2024-05-07 16:40:35 +0200 | <ski> | to prove meta-theorems. Agda is a dependently typed language based on functional programming, rather than logic programming) |
| 2024-05-07 16:40:28 +0200 | <ski> | (lambdaProlog is a logic programming language with support for lambda terms (including (incomplete) unification), you can use this to do HOAS (higher-order abstract syntax), including being able to match under the (meta-)lambdas. Twelf is like a dependently typed version of lambdaProlog, kinda. but you can still do ordinary logic programming in it, e.g. to search for proofs. you can also use its mode system |
| 2024-05-07 16:40:03 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 16:37:40 +0200 | <ski> | (experimenting with type systems stuff can also be fun to do, in e.g. lambdaProlog, Twelf, Agda, or somesuch) |
| 2024-05-07 16:36:23 +0200 | <ski> | or fiddling around with trying to encode some effect of feature, in terms of existing Haskell language features or extensions |
| 2024-05-07 16:35:42 +0200 | <ski> | e.g. writing your own type system or language prototypes |
| 2024-05-07 16:35:28 +0200 | <ski> | you can experiment with a lot of things, in Haskell |
| 2024-05-07 16:34:54 +0200 | <ski> | val foo : 'a -> 'omega as 'a = <fun> |
| 2024-05-07 16:34:52 +0200 | <ski> | # let foo : 'tau -> 'omega as 'tau = fun x -> x x;; |
| 2024-05-07 16:34:38 +0200 | <ski> | - : ('a -> 'b as 'a) -> 'b = <fun> |
| 2024-05-07 16:34:36 +0200 | <ski> | # fun x -> x x;; |
| 2024-05-07 16:34:27 +0200 | <Franciman> | also, do get me for an expert, i'm just learning, and i was wondering whether i could use haskell to experiment |
| 2024-05-07 16:33:38 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 16:31:00 +0200 | <Franciman> | as the word says: fun! |
| 2024-05-07 16:30:52 +0200 | <ski> | (this works with `ocaml -rectypes', if you try `fun x -> x x') |
| 2024-05-07 16:30:27 +0200 | <ski> | (\x. x x) : tau where tau = tau -> omega |
| 2024-05-07 16:30:25 +0200 | <Franciman> | so in there, x : [sigma, [sigma]-> tau] |
| 2024-05-07 16:30:11 +0200 | <Franciman> | it has type [[sigma], [sigma]->tau] -> tau |
| 2024-05-07 16:29:49 +0200 | <Franciman> | (\x. x x) |
| 2024-05-07 16:29:46 +0200 | <Franciman> | yes ski |
| 2024-05-07 16:29:39 +0200 | <ski> | i'm wondering about an example of a term with an intersection type of `sigma' and `tau', where those two are not identical types |
| 2024-05-07 16:29:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 16:28:59 +0200 | <Franciman> | multi-types is related to linear logic and resource management |
| 2024-05-07 16:28:52 +0200 | <Franciman> | EXACTLY |
| 2024-05-07 16:28:36 +0200 | <Franciman> | that's where things get kinda interesting :D |
| 2024-05-07 16:28:30 +0200 | <Franciman> | ski: eheheh, you can use the non-idempotence to count the number of occurrences of a term |
| 2024-05-07 16:28:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |