al-damiri has quit [Quit: Connection closed for inactivity]
<sveit>
Is anyone aware of an up to date timescale/road map for modular implicits?
Ayey_ has joined #ocaml
camelxcore has quit [Ping timeout: 260 seconds]
camelxcore has joined #ocaml
BitPuffin|osx has quit [Ping timeout: 240 seconds]
Ayey_ has quit [Ping timeout: 260 seconds]
shinnya has joined #ocaml
Ayey_ has joined #ocaml
moei has quit [Quit: Leaving...]
Ayey_ has quit [Ping timeout: 240 seconds]
taostein has quit [Quit: taostein]
jabroney has left #ocaml [#ocaml]
mfp has quit [Ping timeout: 240 seconds]
richi235 has quit [Ping timeout: 258 seconds]
nomicflux has joined #ocaml
Ayey_ has joined #ocaml
trapz has joined #ocaml
Ayey_ has quit [Ping timeout: 240 seconds]
marsam has joined #ocaml
shinnya has quit [Ping timeout: 240 seconds]
Ayey_ has joined #ocaml
Ayey_ has quit [Ping timeout: 240 seconds]
taostein has joined #ocaml
chatter29 has joined #ocaml
<chatter29>
hey guys
<chatter29>
allah is doing
<chatter29>
sun is not doing allah is doing
<chatter29>
to accept Islam say that i bear witness that there is no deity worthy of worship except Allah and Muhammad peace be upon him is his slave and messenger
chatter29 has quit [Killed (Sigyn (Spam is off topic on freenode.))]
infinity0 has quit [Ping timeout: 256 seconds]
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
wu_ng has joined #ocaml
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
taostein has quit [Quit: taostein]
marsam has quit [Remote host closed the connection]
trapz has quit [Quit: trapz]
wagle has quit [Read error: Connection reset by peer]
wagle has joined #ocaml
taostein has joined #ocaml
MercurialAlchemi has joined #ocaml
mengu has quit [Remote host closed the connection]
copy` has quit [Quit: Connection closed for inactivity]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
jao has quit [Ping timeout: 240 seconds]
vtomole has joined #ocaml
zpe has quit [Remote host closed the connection]
argent_smith has joined #ocaml
MercurialAlchemi has joined #ocaml
moei has joined #ocaml
vtomole has quit [Ping timeout: 260 seconds]
taostein has quit [Quit: taostein]
Algebr has joined #ocaml
jnavila has joined #ocaml
Algebr has quit [Ping timeout: 264 seconds]
Ayey_ has joined #ocaml
Simn has joined #ocaml
Ayey_ has quit [Ping timeout: 264 seconds]
Ayey_ has joined #ocaml
Algebr has joined #ocaml
iZsh_ has quit [Ping timeout: 240 seconds]
iZsh has joined #ocaml
govg has joined #ocaml
alfredo has joined #ocaml
tane_ has joined #ocaml
Ayey_ has quit [Quit: leaving]
tane_ is now known as tane
govg has quit [Ping timeout: 260 seconds]
govg has joined #ocaml
taostein has joined #ocaml
freusque has joined #ocaml
AlexDenisov has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
freusque has quit [Quit: WeeChat 1.7]
freusque has joined #ocaml
zpe has joined #ocaml
freusque has quit [Quit: WeeChat 1.7]
freusque has joined #ocaml
AlexDenisov has joined #ocaml
Guest73809 is now known as micro_
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
AlexDenisov has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
taostein has quit [Quit: taostein]
richi235 has joined #ocaml
taostein has joined #ocaml
AlexDenisov has joined #ocaml
WuTian has joined #ocaml
freusque has quit [Quit: WeeChat 1.7]
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
freusque has joined #ocaml
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
mfp has joined #ocaml
ezgi has joined #ocaml
ezgi has quit [Client Quit]
AlexDenisov has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
polimegalo has quit [Quit: leaving]
freusque has quit [Quit: WeeChat 1.7]
WuTian has quit [Quit: WuTian]
AlexDenisov has joined #ocaml
taostein has quit [Quit: taostein]
ygrek has joined #ocaml
wu_ng has quit [Ping timeout: 256 seconds]
WuTian has joined #ocaml
WuTian has quit [Remote host closed the connection]
tane has quit [Quit: Leaving]
ygrek has quit [Ping timeout: 260 seconds]
Simn has quit [Ping timeout: 264 seconds]
BitPuffin|osx has joined #ocaml
AlexDenisov has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
Simn has joined #ocaml
al-damiri has joined #ocaml
camelxcore has quit [Ping timeout: 240 seconds]
trapz has joined #ocaml
freusque has joined #ocaml
trapz has quit [Client Quit]
zpe has quit [Remote host closed the connection]
freusque has quit [Quit: WeeChat 1.7]
freusque has joined #ocaml
ygrek has joined #ocaml
trapz has joined #ocaml
profan_ is now known as profan
ygrek_ has joined #ocaml
ygrek has quit [Ping timeout: 268 seconds]
snowcrshd has joined #ocaml
nomicflux has joined #ocaml
trapz has quit [Quit: trapz]
AlexDenisov has joined #ocaml
nomicflux has quit [Quit: nomicflux]
trapz has joined #ocaml
mengu has joined #ocaml
jnavila has quit [Read error: Connection reset by peer]
AlexDenisov has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
shinnya has joined #ocaml
AlexDenisov has joined #ocaml
Algebr has quit [Ping timeout: 246 seconds]
sh0t has joined #ocaml
al-damiri has quit [Quit: Connection closed for inactivity]
ciniglio has joined #ocaml
trapz has quit [Quit: trapz]
trapz has joined #ocaml
oriba has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 240 seconds]
spew has joined #ocaml
<oriba>
can the typesystem be extended with ppx-extensions?
<Drup>
No
<Drup>
but you can encode a shitton of stuff :p
<oriba>
example?
BitPuffin has joined #ocaml
<Drup>
No, I will not give you a list
<Drup>
what are you trying to do ?
marsam has joined #ocaml
octachron has joined #ocaml
<oriba>
I asked, because extending type system. So, this option is out anyways.
<apache2>
is there a way to do | (A|B) (foo) -> .... when I have a type like type foo = A of int | B of int | C of ..
<lyxia>
(A foo | B foo)
<apache2>
ok, I was hoping for a shortcut. thx
<oriba>
Drup: the idea was to have the compiler check matching matrix-sizes, e.g. for matrix-multiplication....
<apache2>
I don't think you need to extend the type system to do that
<oriba>
apache2: I thought about using functors
<apache2>
pretty sure you can do it with GADTs?
<octachron>
oriba, it is already possible with OCaml type system, even if it is somehow troublesome
<Drup>
oriba: check out the slap library
<lyxia>
apache2: if the fields have such similar meanings you could redefine foo as type foo = AB of (aorb * int) | ... and aorb = A | B, then you can match on AB ((A | B), foo)
<apache2>
good point
<octachron>
apache2, depending on the requirement, phantom types can be simpler/better than GADTs for type-level natural
<oriba>
Drup: the question cam up more generally; someone talked to me about types as firdst class values and mentioned the language Idris, which allows it.
<apache2>
do you have some good examples of phantom types?
al-damiri has joined #ocaml
<Drup>
well of course idris allows it, that's the point of dependently typed languages
<octachron>
apache2, slap is using phantom types for instance, my experimental tensor library is using a mixture of phantom type for type-level sizes and gadt for multi-indices
<apache2>
thanks!
<Drup>
octachron: we really need to write those posts :p
<octachron>
Drup, I was thinking exactly the same when trying to think of a good and *simple* use of phantom types
<companion_cube>
what about permissions?
<companion_cube>
they are a really nice and simple use of phantom types
<Drup>
octachron: I was more thinking about the fact that, while there are lot's of material, there is neither an easy point of access nor a vaguely decent reading order
argent_smith1 has joined #ocaml
<Drup>
so, it's a bit like "ok, phantom types are used in all those libraries and none of them really explain the type mechanics they really use"
argent_smith2 has joined #ocaml
argent_smith has quit [Ping timeout: 260 seconds]
argent_smith1 has quit [Ping timeout: 264 seconds]
trapz has quit [Quit: trapz]
argent_smith has joined #ocaml
argent_smith1 has joined #ocaml
argent_smith2 has quit [Ping timeout: 240 seconds]
argent_smith3 has joined #ocaml
argent_smith has quit [Ping timeout: 260 seconds]
argent_smith1 has quit [Ping timeout: 246 seconds]
MercurialAlchemi has joined #ocaml
Mercuria1Alchemi has joined #ocaml
richi235 has quit [Ping timeout: 240 seconds]
Mercuria1Alchemi has quit [Ping timeout: 268 seconds]
jao has joined #ocaml
<oriba>
Drup: I looked for "phantom type" in the refman... just one match, and not explained there...
richi235 has joined #ocaml
camelxcore has joined #ocaml
infinity0 has quit [Remote host closed the connection]
<asdf0987>
the worst part is that I had it working temporarily, and like an idiot I forgot to commit it
<def`>
asdf0987: what do you mean by doesn't work? (more generally, Emacs doesn't work :P)
<asdf0987>
completion-at-point works, but if I hover at the end of List. I don't get any suggestions from autocomplete
<def`>
what are the auto-complete sources?
<def`>
so it doesn't work, but the evaluation succeded?
<asdf0987>
I don't know what you mean by auto-complete sources
<asdf0987>
M-x completion-at-point works (if that's what you meant by the evaluation succeeding)
<def`>
I asked for the evaluation of M-x eval-expression (require 'merlin-ac)
<def`>
ac-sources is the list of "providers" that auto-complete queries
<asdf0987>
def`: It just says 'merlin-ac' in the minibuffer
<def`>
It is defined in the variable ac-sources, can you tell what it is set to in your ml buffer?
<asdf0987>
I updated the gist
kamog has joined #ocaml
<def`>
Thanks. Ok, loading succeded, so the problem must just be in the plugging between merlin and auto-complete.
<asdf0987>
I think it's somehow related to "opam user-setup install", because last time I got to this point (where completion-at-point worked but ac didn't) it fixed it
<def`>
What are ac-sources?
<asdf0987>
def`: I'm sorry, I don't know how to query that in emacs. What should I do?
<lapinot>
hi, i read in the paper about implicit modules some stuff about *first class functors*.. i already used first class modules but first class functors did not yet land on ocaml-stable right? having them would be somewhat equivalent to having implicit modules (modulo some syntactic sugar and implicit namespaces)
<Drup>
first class functors work fine
<lapinot>
mhh actually the second part is kinda stupid..
<Drup>
just like modules, you need to unpack before using them
<lapinot>
mhh okay.. i must have written something wrong then, i kept having syntax errors this evening when trying out some of the given code (the expanded unmagical parts)
jao has quit [Remote host closed the connection]
<lapinot>
and on a more theoretical point of view, how well do first-class functors/modules work? As the type system for modules is quite disjoint from normal expressions don't we loose some nice properties of the type system by unifying them?
<Drup>
it's not unified
<Drup>
(if you want to see a system where they are really unified, take a look at 1ML)
<Drup>
the name "first class modules" is quite misleading, I personally prefer "package types". Basically, you make a (more or less opaque) package that contains the module, and you have to provide the module type when packing/unpacking.
<lapinot>
so "val" and "module" are just some ugly opaque constructor/destructors to embed modules
<lapinot>
ok i get it
nightmared has quit [Ping timeout: 258 seconds]
<lapinot>
1ML is interesting, my first impression is that it's an embedding of core into modules (so everything is a module/functor) but with a syntax that make it look like core, is that the idea or should i read more carefully to understand?
<Drup>
It's quite more subtle than that, because inference for modules is undecidable
<Drup>
1ML tries very hard to keep a system where types are mostly inferable (not all of them, since you have modules, but most of it)
<lapinot>
ok, gonna read further the restrictions
jao has joined #ocaml
<lapinot>
since modules contain types as first-class values, programming only with modules is quite like coq no (which is on the opposite side where almost no inference is possible and you have to prove what you define)?
<Drup>
well, except the module system is not meant to be used for that kind of stuff, yeah, it's a mini-almost-dependently-typed language
<Drup>
(Coq is a lot better at that job, both for practical and theoretic reasons :p)
<lapinot>
makes sense! anyway thanks for answering my many questions lately, i'm very enthousiastic about type theories but i don't have lots in-depth classes about that currently
Simn has quit [Quit: Leaving]
<orbifx>
Drup: lol, yeah them too
<orbifx>
now I'm stuck listenin to Mastodon
marsam has quit [Remote host closed the connection]