Newest at the top
| 2024-05-07 17:37:25 +0200 | Square3 | (~Square4@user/square) |
| 2024-05-07 17:37:06 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 17:36:48 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 17:35:38 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) |
| 2024-05-07 17:27:54 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) (Ping timeout: 255 seconds) |
| 2024-05-07 17:27:38 +0200 | <kuribas> | A statically typed prolog sounds appealing :) |
| 2024-05-07 17:27:21 +0200 | <kuribas> | Or are they more theorem provers/research languages? |
| 2024-05-07 17:27:09 +0200 | <kuribas> | Can you program in these languages? |
| 2024-05-07 17:21:43 +0200 | falafel | (~falafel@211.184.50.36) (Ping timeout: 260 seconds) |
| 2024-05-07 17:14:24 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 2024-05-07 17:13:49 +0200 | Mach | (~Mach@86.127.202.233) |
| 2024-05-07 17:10:16 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-05-07 17:10:08 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 17:10:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-07 17:08:28 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) |
| 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 |