andreypopp has quit [Quit: ZNC 1.7.2+deb3 - https://znc.in]
towel_ has quit [Ping timeout: 252 seconds]
towel has joined #ocaml
adanwan_ has joined #ocaml
adanwan has quit [Remote host closed the connection]
mbuf has joined #ocaml
favonia has quit [Ping timeout: 240 seconds]
favonia has joined #ocaml
waleee has quit [Ping timeout: 240 seconds]
favonia has quit [Ping timeout: 240 seconds]
favonia has joined #ocaml
wingsorc has quit [Quit: Leaving]
zerotypic has quit [Ping timeout: 272 seconds]
adanwan_ has quit [Quit: _]
adanwan has joined #ocaml
Guest9910 has quit [Quit: Konversation terminated!]
spip has joined #ocaml
spip is now known as Guest8235
gravicappa has joined #ocaml
eight has quit [Quit: leaving]
marinelli[m] has quit [Quit: node-irc says goodbye]
favonia has quit [Ping timeout: 256 seconds]
favonia has joined #ocaml
favonia has quit [Ping timeout: 240 seconds]
marinelli[m] has joined #ocaml
shawn has quit [Ping timeout: 272 seconds]
zerotypic has joined #ocaml
olle has joined #ocaml
mro has joined #ocaml
Haudegen has joined #ocaml
mro has quit [Remote host closed the connection]
vizard has joined #ocaml
cedric has joined #ocaml
TakinOver has quit [Ping timeout: 272 seconds]
glassofethanol has joined #ocaml
TakinOver has joined #ocaml
vicfred has quit [Quit: Leaving]
radiopotin[m] has quit [Quit: node-irc says goodbye]
Sumera[m] has quit [Quit: node-irc says goodbye]
zerotypic has quit [Ping timeout: 265 seconds]
mro has joined #ocaml
bartholin has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
zerotypic has joined #ocaml
gravicappa has quit [Ping timeout: 258 seconds]
gravicappa has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Ping timeout: 268 seconds]
mbuf has quit [Quit: Leaving]
Anarchos has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
gareppa has joined #ocaml
gareppa has quit [Quit: Leaving]
mro has joined #ocaml
mro_ has joined #ocaml
mro has quit [Ping timeout: 240 seconds]
mro_ has quit [Remote host closed the connection]
Haudegen has joined #ocaml
favonia has joined #ocaml
mro has joined #ocaml
waleee has joined #ocaml
zebrag has joined #ocaml
<d_bot>
<Alistair> Has anyone made a library w/ lists that use phantom types to indicate non-empty / empty lists? e.g. ```ocaml
<d_bot>
<Alistair> type empty = Empty
<d_bot>
<Alistair> type non_empty = Non_empty
<d_bot>
<Alistair>
<d_bot>
<Alistair> type ('a, 's) t =
<d_bot>
<Alistair> | [] : ('a, empty) t
<d_bot>
<Alistair> | ( :: ) : 'a * ('a, 's) t -> ('a, non_empty) t
<d_bot>
<Alistair> ```
<d_bot>
<octachron> `type 'a nonempty_list = (::): 'a * 'a list` is probably simpler while providing the same benefits.
<d_bot>
<octachron> Ok, not completely the same benefits, using a phantom type allows to share `cons`: `cons: 'a -> ('a, _) t -> ('a, non_empty) t`.
<d_bot>
<Alistair> Yeah, and prevents duplicate functions (1 for lists and 1 for non-empty lists)? I was thinking of using it for my `prologue` library (extends Base w/ all the things I miss from other languages) and thought it would be pretty neat way of handling empty and non empty lists
<d_bot>
<octachron> Well, the functions for list already exists. So the battle for preventing duplicates is already lost.
<d_bot>
<octachron> Note that writing the function/library is certainly a fun endeavor, it is just not clear if the complexity is worth it.
<d_bot>
<octachron> And answering the initial question, I am not sure if such library exists. But that is a generic issues with heterogeneous lists: they are so many subtle variants on those that most implementations are ad-hoc.
<d_bot>
<octachron> Another interesting to implement such lists would be to write a size-counting heterogeneous list functor with `zero = empty` and `'a succ = non_empty`.
<d_bot>
<Alistair> Yeah, that would also work nicely as well
Tuplanolla has joined #ocaml
insep has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
glassofethanol has quit [Quit: leaving]
eight has joined #ocaml
berberman_ has joined #ocaml
berberman has quit [Ping timeout: 256 seconds]
olle has quit [Ping timeout: 256 seconds]
chrde has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Remote host closed the connection]
<chrde>
I am writing a parser (menhir, ocamlex) for a language (plpgsql) that allows an arbitrary amount of nested statements delimited by $<label>$, e.g
<chrde>
$first$
<chrde>
some code here
<chrde>
$second$
<chrde>
more code here
<chrde>
$second$
<chrde>
even more code here
<chrde>
$first$
<chrde>
Is there a way to encode the restriction that every label must be closed, within menhir?
EmoSpice6 is now known as EmoSpice
Haudegen has joined #ocaml
bartholin has quit [Quit: Leaving]
vizard has quit [Ping timeout: 258 seconds]
olle has joined #ocaml
elf_fortrez has joined #ocaml
<dmbaturin>
chrde: As in, have a $ on both sides?
<dmbaturin>
There's a delimited() macro.
<chrde>
$one$ hello $two$ <eof>
<chrde>
this should be invalid, because there is no 'closing' $one$
<chrde>
$one$ hello $one$ <eof>
<chrde>
this is valid
<chrde>
at the moment I keep a set of open labels in a global variable, but it'd be nice if I could encode this restriction somehow in menhir/ocamllex
<octachron>
I don't think there is a way without keeping a list of opened tags somewhere. However, you can probably restrict this state to the lexing code and emits Open/Close tokens for the parser.
<dmbaturin>
Oh, I get what you mean now.
<dmbaturin>
Yeah, looks like a lexer hack time to me.
<octachron>
You can also probably keep only the last token depending on the interpretation of $a$ $b$ $a$ $a$ $b$ $a$
<dmbaturin>
That grammar would be context-free over a set of tokens like Label(<name>) ... EndLabel; and the lexer can take care of the non-context-free bit.
<chrde>
makes sense; thanks
elf_fortrez has quit [Quit: Client closed]
olle_ has joined #ocaml
marinelli[m] has quit [Quit: node-irc says goodbye]
chrde has quit [Quit: Client closed]
jtck has quit [Remote host closed the connection]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
insep has quit [Read error: Connection reset by peer]
insep has joined #ocaml
insep has quit [Read error: Connection reset by peer]
insep has joined #ocaml
marinelli[m] has joined #ocaml
greenbagels has joined #ocaml
greenbagels has quit [Changing host]
insep has quit [Read error: Connection reset by peer]
insep has joined #ocaml
insep has quit [Client Quit]
Stumpfenstiel has joined #ocaml
Anarchos has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
gravicappa has quit [Ping timeout: 272 seconds]
Stumpfenstiel has quit [Quit: No Ping reply in 180 seconds.]
Stumpfenstiel has joined #ocaml
jinsun has quit [Ping timeout: 256 seconds]
mro has joined #ocaml
olle has quit [Ping timeout: 240 seconds]
<d_bot>
<Alistair> Did a bit more reading in GADTs, I've got this so far: ```ocaml
<d_bot>
<Alistair> | ( :: ) : 'a * ('a, 'n) list -> ('a, 'n s) list
<d_bot>
<Alistair>
<d_bot>
<Alistair> let rec length : type a n. (a, n) list -> n nat =
<d_bot>
<Alistair> function
<d_bot>
<Alistair> | [] -> Zero
<d_bot>
<Alistair> | _ :: xs -> Succ (length xs)
<d_bot>
<Alistair>
<d_bot>
<Alistair> let head : type a n. (a, n s) list -> a = function
<d_bot>
<Alistair> | x :: _ -> x
<d_bot>
<Alistair>
<d_bot>
<Alistair> let tail : type a n. (a, n s) list -> (a, n) list = function
<d_bot>
<Alistair> | _ :: xs -> xs
<d_bot>
<Alistair>
<d_bot>
<Alistair> let rec map : type a b n. (a, n) list -> f:(a -> b) -> (b, n) list =
<d_bot>
<Alistair> fun xs ~f -> match xs with
<d_bot>
<Alistair> | [] -> []
<d_bot>
<Alistair> | x :: xs -> f x :: map xs ~f
<d_bot>
<Alistair>
<d_bot>
<Alistair> (** This define defines the existential type [exists n. ('a, n) list] *)
<d_bot>
<Alistair> type _ exists_list =
<d_bot>
<Alistair> | Exists_list : ('a, 'n) list -> 'a exists_list
<d_bot>
<Alistair>
<d_bot>
<Alistair> let rec filter : type a n. (a, n) list -> f:(a -> bool) -> a exists_list =
<d_bot>
<Alistair> fun xs ~f -> match xs with
<d_bot>
<Alistair> | [] -> Exists_list []
<d_bot>
<Alistair> Is there a better way of doing `append`? Seems a bit fiddly
<d_bot>
<octachron> You should use a copy-paste site rather on #general . Your type `Exists_list` is essentially a normal list: the existential quantification has erased the type-level size information.
<d_bot>
<octachron> One option is to use: https://drup.github.io/2016/08/02/difflists/ (which is is essentially replacing the unary representation of integer by an unary representation of translation on the integers). But with the lack of value restriction for GADTs that works less well than expected on first reading.
<d_bot>
<octachron> Note that the code sharing restriction is here for the irc bridge. With the current(?) limitation of time travel technology, editing the post at posteriori is not needed.
mro has quit [Read error: Connection reset by peer]
mro has joined #ocaml
<d_bot>
<Alistair> Oh neat, I see, so much `'n` is equiv to n arrows in the diff list representation.
<d_bot>
<octachron> Another interesting point to notice is that the difficulty with `append` also applies with your initial empty/non_empty list.
<d_bot>
<Alistair> What do you mean by "the lack of value restrictions for GADT that works less well than expected ..."?
<d_bot>
<octachron> In this case, concatenation is using the "tail" type variable to compute the "append" at the type level. When this type variable is not generic, this means that each append consumes the type variable and it cannot used for another appends.
<d_bot>
<octachron> And since GADTs are not afforded the relaxed value restriction (due to the lack of variance), every list produced by a function is not polymorph. Thus the issue above happens all the time.
<d_bot>
<Alistair> I see, shame it doesn't really work out