rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
Sankalp has quit [Ping timeout: 252 seconds]
Sankalp has joined #ocaml
williewillus_ has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
waleee has quit [Ping timeout: 240 seconds]
zebrag has quit [Read error: Connection reset by peer]
zebrag has joined #ocaml
rgrinberg has joined #ocaml
rgrinberg has quit [Client Quit]
rgrinberg has joined #ocaml
chrisz has quit [Ping timeout: 272 seconds]
chrisz has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
nvaxplus has joined #ocaml
rgrinberg has joined #ocaml
<nvaxplus>
I have a somewhat contrived question about GADTs. I'm trying to define a GADT that has a constructor for both arrays and bytes so I can abstract over the underlying representation. However, for some objects only some operations are relevant for bytes
<nvaxplus>
Here's my code
<nvaxplus>
type 'a gadt_array =
<nvaxplus>
| GArray : 'a array -> 'a gadt_array
<nvaxplus>
| GBytes : bytes -> char gadt_array
<nvaxplus>
let get_int8 (GBytes b: char fast_array) i = Bytes.get_int16_le b i
<nvaxplus>
I get an exhaustiveness error for this. I think I understand why. You could have a Garray where 'a is instantiated with char too, but is there any way to define get_int16 (typo in my above code) *only* for GBytes?
rgrinberg has quit [Ping timeout: 245 seconds]
<nvaxplus>
I guess I could make the constructor to GBytes have type unit * bytes -> gadt_array
<nvaxplus>
to differentiate between the two
<d_bot>
<darrenldl> maybe try swapping the right 'a with some dummy type?
<d_bot>
<darrenldl>
<d_bot>
<darrenldl> iirc it does not impact what your constructor can store, and the return type is only used as an index
<d_bot>
<darrenldl> but i am not a regular user of gadt so i might be saying complete nonsense
<d_bot>
<NULL> I think it makes more sense to make the bytes special case more special if you need it, but then I don't really get what GADTs can bring that a regular variant wouldn't
rgrinberg has joined #ocaml
rgrinberg has quit [Ping timeout: 272 seconds]
azimut has joined #ocaml
mbuf has joined #ocaml
<nvaxplus>
darrendl: the problem is that doesn't that make the 'a existential?
williewillus_ has quit [Quit: Leaving]
jpds1 has quit [Ping timeout: 268 seconds]
jpds1 has joined #ocaml
trev has joined #ocaml
<d_bot>
<darrenldl> ah right indeed
adanwan has quit [Remote host closed the connection]
adanwan has joined #ocaml
jpds1 has quit [Read error: Connection reset by peer]
adanwan has quit [Remote host closed the connection]
adanwan has joined #ocaml
jpds1 has joined #ocaml
Sankalp has left #ocaml [#ocaml]
Exa has quit [*.net *.split]
dstein64 has quit [*.net *.split]
sparogy has quit [*.net *.split]
berberman has quit [*.net *.split]
welterde has quit [*.net *.split]
sparogy has joined #ocaml
Exa has joined #ocaml
welterde has joined #ocaml
berberman has joined #ocaml
dstein64 has joined #ocaml
rgrinberg has joined #ocaml
Haudegen has joined #ocaml
<octachron>
nvaxplus, you have two implementations of `char gadt_array`, and no information at type-level for distinguishing the two. The solution is thus to add this information at type level with a type-level tag for instance.
<nvaxplus>
I see yes. So would I make a variant with a single constructor and change the signature of GBytes to be like, Tag * bytes -> (tag * char) gadt_array?
<octachron>
type ('elt,'kind) gadt_array = Bytes: Bytes.t -> (char,[`compact]) gadt_array
<nvaxplus>
oooooh I see
<nvaxplus>
that makes sense
<octachron>
with a polymorphic variant, but type compact = private Compact_tag works too.
h11 has quit [*.net *.split]
megeve has quit [*.net *.split]
greenbagels has quit [*.net *.split]
v0idpwn has quit [*.net *.split]
Boarders__ has quit [*.net *.split]
Geekingfrog has quit [*.net *.split]
Duns_Scrotus has quit [*.net *.split]
kandu has quit [*.net *.split]
daimrod has quit [*.net *.split]
sim642 has quit [*.net *.split]
towel has quit [*.net *.split]
adanwan has quit [Remote host closed the connection]
daimrod has joined #ocaml
v0idpwn has joined #ocaml
kandu has joined #ocaml
greenbagels has joined #ocaml
<nvaxplus>
I see, are there any advantages to the private type version?
Duns_Scrotus has joined #ocaml
greenbagels has quit [Changing host]
greenbagels has joined #ocaml
megeve has joined #ocaml
Boarders__ has joined #ocaml
sim642 has joined #ocaml
Geekingfrog has joined #ocaml
adanwan has joined #ocaml
rgrinberg has quit [Ping timeout: 255 seconds]
<octachron>
the private annotation is here to indicate that the type is only here for type-level programming, but otherwise both options are mostly equivalent.
towel has joined #ocaml
h11 has joined #ocaml
<nvaxplus>
I see. Thank you again, this is very helpful!
dnh has joined #ocaml
rgrinberg has joined #ocaml
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
gopiandcode has quit [Ping timeout: 276 seconds]
gopiandcode has joined #ocaml
rgrinberg has quit [Ping timeout: 255 seconds]
Serpent7776 has joined #ocaml
nvaxplus__ has joined #ocaml
nvaxplus has quit [Read error: Connection reset by peer]
gopiandcode has quit [Ping timeout: 252 seconds]
gopiandcode has joined #ocaml
nvaxplus__ has quit [Quit: Leaving]
kakadu has joined #ocaml
azimut has quit [Remote host closed the connection]
azimut has joined #ocaml
dnh has joined #ocaml
azimut has quit [Remote host closed the connection]
azimut_ has joined #ocaml
Anarchos has joined #ocaml
jpds1 has quit [Ping timeout: 268 seconds]
jpds1 has joined #ocaml
<d_bot>
<ansiwen> if I have a `type 'a t` and later I want to construct a concrete type that is also called `t`, like `type t = int t`, is there a trick or syntax to do that directly, without using an intermediate type name? (because `type t' = int t ;; type t = t'` _does_ work.)
bartholin has joined #ocaml
omegatron has joined #ocaml
<d_bot>
<octachron> `type nonrec t = int t`
gopiandcode has quit [Read error: Connection reset by peer]
gopiandcode has joined #ocaml
<d_bot>
<ansiwen> Thank you so much! It's so difficult to google for these things, if you don't know the answer already.
rgrinberg has joined #ocaml
rgrinberg has quit [Ping timeout: 268 seconds]
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
dnh has joined #ocaml
bartholin has quit [Ping timeout: 268 seconds]
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
xgqt has quit [Ping timeout: 245 seconds]
xgqt has joined #ocaml
bartholin has joined #ocaml
jpds1 has quit [Write error: Connection reset by peer]
dnh has joined #ocaml
jpds1 has joined #ocaml
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
dnh has joined #ocaml
Tuplanolla has joined #ocaml
gwizon has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
bartholin has quit [Ping timeout: 252 seconds]
trev has quit [Quit: trev]
trev has joined #ocaml
jpds1 is now known as jpds
bartholin has joined #ocaml
spip has joined #ocaml
bobo_ has quit [Ping timeout: 245 seconds]
szkl has joined #ocaml
olle has joined #ocaml
Haudegen has joined #ocaml
hasbae is now known as hippoid
rgrinberg has joined #ocaml
CodeBitCookie[m] is now known as bitblit
yilin has joined #ocaml
bartholin has quit [Ping timeout: 245 seconds]
azimut_ has quit [Remote host closed the connection]
azimut has joined #ocaml
bartholin has joined #ocaml
rgrinberg has quit [Ping timeout: 240 seconds]
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
Haudegen has quit [Quit: Bin weg.]
d_bot has quit [Ping timeout: 260 seconds]
motherfsck has quit [Ping timeout: 245 seconds]
rgrinberg has joined #ocaml
zebrag has joined #ocaml
motherfsck has joined #ocaml
yilin has quit [Ping timeout: 240 seconds]
adanwan has quit [Quit: _]
adanwan has joined #ocaml
dnh has joined #ocaml
sonologico has joined #ocaml
Serpent7776 has quit [Quit: WeeChat 1.9.1]
sonologico has quit [Ping timeout: 240 seconds]
sonologico has joined #ocaml
Haudegen has joined #ocaml
sonologico has quit [Ping timeout: 240 seconds]
bartholin has quit [Ping timeout: 268 seconds]
sonologico has joined #ocaml
sonologico has quit [Ping timeout: 240 seconds]
mbuf has quit [Quit: Leaving]
trev has quit [Remote host closed the connection]
<companion_cube>
hmm, I guess most people are on vacation… Drup are you, too?
Anarchos has quit [Quit: Vision[]: i've been blurred!]
bartholin has joined #ocaml
yilin has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
cedb has joined #ocaml
<cedb>
ive been rereading Pierce's TAPL but I'm finding it a bit pedantic for my taste, any alternative recommandations?
yilin has quit [Ping timeout: 245 seconds]
bartholin has quit [Ping timeout: 240 seconds]
Tuplanolla has quit [Quit: Leaving.]
bartholin has joined #ocaml
motherfsck has quit [Ping timeout: 268 seconds]
yilin has joined #ocaml
adanwan has quit [Write error: Connection reset by peer]
adanwan has joined #ocaml
<hippoid>
cedb: I'd be intesreted as well. I'm reading it for the first time and translating into haskell
<cedb>
hippoid: ill give thompsons "type theory and functional programming" a shot, can let you know how it feels
<hippoid>
cedb: didnt know of that one... ill check it out. you might try thinkingwithtypes.com, I own a copy and I'm saving it for after I get through tapl
<yilin>
hippoid: I think Wadler did a translation a while back?
<yilin>
For Agda
<yilin>
Uh, I think I'm thinking of PLF rather than TAPL