<mengu>
kerrhau: let me know if you need any more help
sam_ has joined #ocaml
sam_ has quit [Ping timeout: 248 seconds]
sam_ has joined #ocaml
peterpp has joined #ocaml
copy_ has quit [Quit: Connection closed for inactivity]
peterpp has quit [Ping timeout: 240 seconds]
sam_ has quit [Ping timeout: 248 seconds]
coventry has joined #ocaml
<coventry>
Is there a way to get at structures which are hidden by the interface file, for instance, in order to write tests which depend on module internals?
pierpa has quit [Quit: Page closed]
coventry has quit [Read error: Connection reset by peer]
enterprisey has joined #ocaml
TarVanimelde has joined #ocaml
mengu has quit [Quit: Leaving...]
mfp__ has quit [Ping timeout: 246 seconds]
jao has quit [Ping timeout: 240 seconds]
<benzrf>
oh god i just realized that it must matter what order you put bindings in
<benzrf>
:\
sam_ has joined #ocaml
<benzrf>
begone control flow
sam_ has quit [Ping timeout: 260 seconds]
samrat has joined #ocaml
jlam__ has joined #ocaml
jlam1 has quit [Ping timeout: 240 seconds]
TarVanimelde has quit [Quit: TarVanimelde]
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
MercurialAlchemi has joined #ocaml
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
rageoholic has joined #ocaml
TarVanim_ has joined #ocaml
TarVanim_ has quit [Client Quit]
<rageoholic>
Hey I've run into an issue with utop. So according to Real World OCaml, utop will handle all the async stuff in the background. However, this appears to no longer be the case? Like let three = return 3;; three;; shows me a Deferred.t and not an int.
govg has quit [Ping timeout: 240 seconds]
ShalokShalom has joined #ocaml
rageoholic has left #ocaml ["ERC (IRC client for Emacs 25.2.50.2)"]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
KeyJoo has quit [Ping timeout: 255 seconds]
kerrhau has quit [Ping timeout: 260 seconds]
Associat0r has quit [Ping timeout: 240 seconds]
sam_ has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 240 seconds]
sam_ has quit [Ping timeout: 240 seconds]
mbuf has joined #ocaml
MercurialAlchemi has joined #ocaml
coventry has joined #ocaml
<coventry>
Are there any tools in OCaml for randomly generating member types of GADT's? E.g., if I have a "type 'a gadt = | Unit : unit gadt | Bool : bool gadt" it would somehow randomly generate either Unit or Bool, maybe by saving it out to an autogenerated .ml file and compiling it.
<coventry>
Simple enough in this example, but it gets more complex with recursive GADT's.
enterprisey has quit [Read error: Connection reset by peer]
BitPuffin|osx has quit [Remote host closed the connection]
zlsyx has joined #ocaml
zv has quit [Ping timeout: 246 seconds]
<zlsyx>
Let the type ('a*'b) list describe a list of pairs where the first components of pairs
<zlsyx>
are keys of type 'a and the second components are the values of type 'b.
<zlsyx>
What kind of type is ('a * 'b)? Isn't that a tuple of 2 lists?
sam_ has joined #ocaml
BitPuffin|osx has joined #ocaml
TheLemonMan has joined #ocaml
troydm has quit [Ping timeout: 255 seconds]
<reynir>
'a * 'b is a pair with two type variables 'a and 'b
sam_ has quit [Ping timeout: 246 seconds]
<zlsyx>
Where can I read more about this, it really doesn't make sense, why not (int * int) ?
ygrek has quit [Remote host closed the connection]
ygrek has joined #ocaml
<maelkum>
zlsyx: I guess because sometimes the inferencer can't deduce the type, so it inserts type variables instead of concrete types
mfp__ has joined #ocaml
zv has joined #ocaml
<maelkum>
zlsyx: but it's just a guess, I only received my copy of Real World OCaml yesterday ;-)
SomeDamnBody has quit [Remote host closed the connection]
ygrek has quit [Remote host closed the connection]
<zlsyx>
How do you get the key of a pair (1, 2) for example?
<zlsyx>
it should be 1
<maelkum>
let p = (1, 2);;
<maelkum>
fst p;;
<maelkum>
fst is the function to get first element of a pair
<zlsyx>
So ('a * 'b) list is a list of pairs like [(1, 2); (3,4)];;
<maelkum>
I think so
<flux>
correct
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
Mercuria1Alchemi has joined #ocaml
<wklm>
IG
<wklm>
sorry
nconc has joined #ocaml
<nconc>
hello, is it possible to use C allocated memory in ocaml through ffi without copying
troydm has joined #ocaml
argent_smith1 has joined #ocaml
ShalokShalom_ has joined #ocaml
argent_smith has quit [Ping timeout: 260 seconds]
ShalokShalom has quit [Ping timeout: 252 seconds]
kakadu has joined #ocaml
troydm has quit [Ping timeout: 248 seconds]
<mrvn>
nconc: sure. Bigarray uses that for example.
<mrvn>
or the ctypes module
<nconc>
so if i use the bigarray alloc function in the C stub, then gc will take care of that memory?
<mrvn>
nconc: If you use the bigarry alloc function then you get a bigarry with all that entails. If you need something else look at custom blocks with finalizer
<mrvn>
Chapter 19.9 in the manual
<zlsyx>
type 'a bin_tree =
<zlsyx>
Empty
<zlsyx>
| Node of 'a bin_tree * 'a * 'a bin_tree ;;
<mrvn>
"type 'a bin_tree" says the bin_tree has a type variable 'a. After that you can use 'a on the other side.
<mrvn>
You need "type ('a * 'b) pair = ..."
<zlsyx>
What does type variable 'a mean?
<zlsyx>
Like I'm sorry if it's a dumb question but is it like unspecified type like a placeholder or something?
<zlsyx>
could be either string or int
<mrvn>
or float or 'a bin_tree or whatever. It's a placeholder
troydm has joined #ocaml
troydm has quit [Ping timeout: 260 seconds]
zlsyx has quit [Remote host closed the connection]
samrat has quit [Ping timeout: 240 seconds]
zlsyx has joined #ocaml
troydm has joined #ocaml
TheLemonMan has quit [Quit: "It's now safe to turn off your computer."]
nconc has quit [Quit: Page closed]
sam_ has joined #ocaml
<rwmjones>
sgnb: to close the loop on the jbuilder package (which I see has also been added to Debian), this is the Fedora package: https://src.fedoraproject.org/rpms/jbuilder
ziyourenxiang has joined #ocaml
troydm has quit [Ping timeout: 240 seconds]
troydm has joined #ocaml
troydm has quit [Ping timeout: 240 seconds]
jlam__ has quit [Ping timeout: 246 seconds]
jlam has joined #ocaml
jlam is now known as Guest38908
Guest38908 has quit [Killed (card.freenode.net (Nickname regained by services))]
jlam_ is now known as jlam
jlam_ has joined #ocaml
theblatte has joined #ocaml
eh_eff has joined #ocaml
eh_eff has quit [Ping timeout: 246 seconds]
troydm has joined #ocaml
_andre has joined #ocaml
mbuf has quit [Quit: Leaving]
jbrown has joined #ocaml
dave_tucker has quit []
rossberg has quit [Ping timeout: 252 seconds]
sz0 has joined #ocaml
KeyJoo has joined #ocaml
rossberg has joined #ocaml
troydm has quit [Ping timeout: 240 seconds]
samrat has joined #ocaml
Lightsephi has joined #ocaml
Associat0r has joined #ocaml
Associat0r has quit [Changing host]
Associat0r has joined #ocaml
zv has quit [Ping timeout: 255 seconds]
troydm has joined #ocaml
samrat has quit [Ping timeout: 264 seconds]
ShalokShalom_ is now known as ShalokShalom
zv has joined #ocaml
sepp2k has quit [Quit: Leaving.]
sh0t has joined #ocaml
jao has joined #ocaml
zlsyx has quit [Quit: Leaving...]
samrat has joined #ocaml
AltGr has joined #ocaml
philtor has joined #ocaml
sh0t has quit [Ping timeout: 246 seconds]
benzrf has left #ocaml ["WeeChat 1.9"]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
govg has quit [Ping timeout: 240 seconds]
govg has joined #ocaml
FreeBirdLjj has joined #ocaml
sh0t has joined #ocaml
govg has quit [Ping timeout: 240 seconds]
AltGr has left #ocaml [#ocaml]
govg has joined #ocaml
jlam__ has joined #ocaml
malina has joined #ocaml
jlam_ has quit [Ping timeout: 240 seconds]
jlam_ has joined #ocaml
jlam__ has quit [Ping timeout: 248 seconds]
TobiasBales has quit [Ping timeout: 240 seconds]
jlam__ has joined #ocaml
jlam_ has quit [Ping timeout: 260 seconds]
jlam__ has quit [Ping timeout: 240 seconds]
jao has quit [Ping timeout: 264 seconds]
AltGr has joined #ocaml
troydm has quit [Ping timeout: 240 seconds]
TheLemonMan has joined #ocaml
mbuf has joined #ocaml
kerrhau has joined #ocaml
AltGr has left #ocaml [#ocaml]
sz0 has quit [Quit: Connection closed for inactivity]
sepp2k has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
troydm has joined #ocaml
ShalokShalom has quit [Ping timeout: 248 seconds]
Mercuria1Alchemi has quit [Ping timeout: 260 seconds]
FreeBirdLjj has joined #ocaml
jao has joined #ocaml
ShalokShalom has joined #ocaml
eh_eff has joined #ocaml
gpietro has joined #ocaml
sh0t has quit [Read error: Connection reset by peer]
<Armael>
indeed it doesn't seem to appear in the list you linked
<kakadu>
OKay, I'm not worried now
<kakadu>
do you know will it be streamed?
<Armael>
mmm, I'm not sure
FreeBirdLjj has quit [Remote host closed the connection]
<Drup>
OCaml workshop will not be streamed, but it will be recorded and uploaded
<flux>
hopefully with better video/audio quality than in other similar events :/
AltGr has joined #ocaml
<kakadu>
Current quality of ICFP stream is fine
<flux>
great to hear
AltGr has left #ocaml [#ocaml]
<reynir>
The MOOC talk had really bad audio though
kakadu has quit [Quit: Konversation terminated!]
SomeDamnBody has joined #ocaml
<SomeDamnBody>
Is it possible to pass an argument from opam to oasis somehow?
<SomeDamnBody>
Like, in the opam, I can use a variable based on the os to change the command. I need a particular flag to be defined for a CC lib that is different based on the platform
<SomeDamnBody>
But, it's oasis that actually builds the C source.
coventry has joined #ocaml
rageoholic has joined #ocaml
<rageoholic>
Hi I asked this last night but I had to sleep before I got an answer. So Real World OCaml says that utop will resolve Async.Std.Deferred.t but it seems that this behavior has changed? Is there any way to force utop to emulate the old behavior?
dmj` has quit []
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
malina has quit [Remote host closed the connection]
roo1 has joined #ocaml
<roo1>
is lists are immutable in FP ?
<coventry>
rageoholic: Do you have utop set up to include Jane Street's Core?
<thizanne>
roo1: ocaml lists are, and what we call "lists" usually are in functional languages
<roo1>
is list are efficient ?
<coventry>
roo1: Really depends on what you're doing.
<thizanne>
(although you could easily implement mutable doubly linked lists, but that's not really idiomatic since you do not gain anything by doing so)
malina has joined #ocaml
<roo1>
creating new list everytime construct/de will be bad for memory
<thizanne>
roo1: you should not care about it until you have to care about it
<thizanne>
(but they were made immutable in newer versions since mutability is of little use and makes reasoning about code much harder)
<thizanne>
(and probably also for optimisation reasons)
<roo1>
even in haskell wont it hit bad ?
<thizanne>
haskell has a type for efficiently implemente strings
<kerrhau>
is it possible to do something like this? if x > y then foo bar; baz bar; else z x;;?
<thizanne>
and strings as lists of char is usually retrospectively considered as a bad choice
<thizanne>
kerrhau: it is, but put begin/end (or parentheses) around foo bar; baz bar
kakadu has joined #ocaml
<thizanne>
if/then/else binds tighter than ;
kakadu_ has joined #ocaml
<roo1>
but the idea of FP is everything immutable
<roo1>
right
andreas___ has joined #ocaml
sam_ has joined #ocaml
bigs_ has joined #ocaml
redcedar_ has joined #ocaml
<kerrhau>
thizanne: without semicolons?
<thizanne>
it's one idea of what people vaguely define as "FP"
jyc_ has joined #ocaml
<thizanne>
kerrhau: if x > y then begin foo bar; baz bar else z x
<coventry>
roo1: What are you trying to do/learn?
caw__ has joined #ocaml
<thizanne>
you can remplace begin/end by (/) that behave exactly the same
<roo1>
doing some challenges in FP
<kerrhau>
thizanne: ohhh okay
<krktz>
(why are strings as char lists a bad idea?)
<thizanne>
kerrhau: another way of doing it is if x > y then let () = foo bar in baz bar else z x
<thizanne>
sometimes it happens to feel nicer
<roo1>
wont i go out of memory soon ?!
theblatt1 has joined #ocaml
<roo1>
with lot of garbage
chelfi2 has joined #ocaml
<coventry>
roo1: No. Persistent data structures work differently than you're used ot.
<roo1>
you cant change the value , since its immutable
<roo1>
and you create a new one
bacam_ has joined #ocaml
<roo1>
wont this cause :!
<roo1>
am i missing anything
<thizanne>
roo1: you're missing the garbage collector
kakadu has quit [Ping timeout: 255 seconds]
<coventry>
Yes, you should read the links I sent you. The key concept is that similar structures share data in memory.
<thizanne>
which automatically releases the parts that are not used anymore (and cant be used in the future there is no way to name them, directly or indirectly)
sam_ has quit [Ping timeout: 246 seconds]
<roo1>
k thank you , ill have look and come around
mbuf has quit [Quit: Leaving]
roo1 has quit [Quit: Leaving]
<coventry>
To be more precise, when you "modify" a portion persistent data structure, the new structure shares most of the old one's representation in memory of the unmodified portions.
<coventry>
portion -> portion of
bitbckt_ has joined #ocaml
bjs_ has joined #ocaml
sigjuice_ has joined #ocaml
theblatte has quit [*.net *.split]
dakk has quit [*.net *.split]
rbocquet has quit [*.net *.split]
Orion3k has quit [*.net *.split]
nullifidian has quit [*.net *.split]
nightmared has quit [*.net *.split]
andreas__ has quit [*.net *.split]
bitbckt has quit [*.net *.split]
bacam has quit [*.net *.split]
sigjuice has quit [*.net *.split]
jyc has quit [*.net *.split]
timclassic has quit [*.net *.split]
chelfi1 has quit [*.net *.split]
bjs has quit [*.net *.split]
bigs has quit [*.net *.split]
caw_ has quit [*.net *.split]
redcedar has quit [*.net *.split]
maufred has quit [*.net *.split]
andreas___ is now known as andreas__
bjs_ is now known as bjs
redcedar_ is now known as redcedar
jyc_ is now known as jyc
bigs_ is now known as bigs
malina has quit [Remote host closed the connection]
bsima has quit [Ping timeout: 260 seconds]
nahra` has joined #ocaml
jao has quit [Disconnected by services]
CrazedProgrammer has quit [Quit: Ping timeout (120 seconds)]
wagle has quit [Quit: No Ping reply in 180 seconds.]
nahra has quit [Remote host closed the connection]
<coventry>
Oh, do I have to universalize the domain and range types of f?
maedoc has joined #ocaml
maedoc has quit [Ping timeout: 248 seconds]
jao has joined #ocaml
maedoc has joined #ocaml
samrat has quit [Ping timeout: 252 seconds]
maedoc has quit [Ping timeout: 248 seconds]
Soni is now known as PornBlog
dakk has quit [Ping timeout: 255 seconds]
<rageoholic>
coventry: Sorry I had to step away for a while. Yeah I have all the .ocamlinit stuff set up.
<rageoholic>
I'm really not sure what the bug is here
sam_ has joined #ocaml
sam_ has quit [Ping timeout: 260 seconds]
pigeonv has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 264 seconds]
<SomeDamnBody>
Is there a way to find out the homebrew folder location from within opam?
<SomeDamnBody>
Imagine someone installs homebrew to a particular directory. Could they specify where on the command line? Or is there any way for me to echo a hint at the command line from within opam if the build fails?
<pigeonv>
SomeDamnBody: opam config var root?
<SomeDamnBody>
pigeonv: ... that's for opam's root
<SomeDamnBody>
I'm looking for identifying where the homebrew folder location is using a command
<pigeonv>
oh I thought it was installed in a subfolder of Homebrew's data (I'm running Debian)
<SomeDamnBody>
homebrew is a package manager for mac.
<pigeonv>
yeah
<SomeDamnBody>
But opam's depext feature can resolve dependencies using homebrew
<pigeonv>
maybe an environment variable is defined somehow?
<pigeonv>
at least, it's in the PATH
<SomeDamnBody>
it's in path
<SomeDamnBody>
Well, I found that brew has a config option
<pigeonv>
and when I don't remember that depext needs the package manager's exact path
<SomeDamnBody>
pigeonv: well, normally homebrew installs to some opt folder. But on my OSX, I have homebrew somewhere else.
<SomeDamnBody>
So, I wanted to make sure that everyone else can get the package but it's hard to test on OSX because it's not like docker. YOu have to remember where you put anything because the environment can't be reset easily
<pigeonv>
yeah, so you installed it twice
<SomeDamnBody>
In any case, brew installed boost, and to get to the headers from a opam driven make invocation, you have to specify where the header folder is.
<pigeonv>
can't you use some chroot?
<pigeonv>
maybe that's a bit excessive
<SomeDamnBody>
pigeonv: "installed it twice" -> I am looking to test the install multiple times. Right now, I've gotten it path pinned successfully. But it's not very portable.
<SomeDamnBody>
possibly chroot would help with testing.
<SomeDamnBody>
But right now, I'm looking at resolving the portability issue.
<pigeonv>
if the dependencies are expressed correctly, people don't have to pin anything
<pigeonv>
except if you're using software newer than the currently published packages
<SomeDamnBody>
pigeonv: right, and I have a Dockerfile where I will use my fork of opam-repository and all that to make sure that pinning isn't necessary
<pigeonv>
in this case, it's a bit of a nightmare haha
<SomeDamnBody>
pigeonv: yes, the software is new. The opam package I just wrote isn't public yet.
<SomeDamnBody>
Well, I'm almost finished with this package. Took me yesterday and today to work through all the issues.
PornBlog is now known as Soni
<pigeonv>
yeah so that's pretty normal, it should work once it's published ;)
jao has quit [Ping timeout: 260 seconds]
<SomeDamnBody>
But I can't publish it until I figure out the best way to find the homebrew path location.
<SomeDamnBody>
I wonder if I should just expect the headers to be in opt/local/include
<pigeonv>
it's strange that you still have to do such platform-specific things
<pigeonv>
I know that on some other platforms, there are tools to get the right path for each packaged library
<SomeDamnBody>
Well, I develop on OSX, but I want to make sure that this works for linux too.
<pigeonv>
and that's the problem
<SomeDamnBody>
Since I want to be able to automate this whole build. My deal is, I want my freaking merlin and emacs to work!
<pigeonv>
on Linux it'll probably be in /usr/include
<SomeDamnBody>
pigeonv: well, usr/include is in the compiler default include directory set.
<pigeonv>
or /usr/local/include if the user compiled the library by himself
<pigeonv>
oops you're right
<SomeDamnBody>
on osx, homebrew and port are usually left out.
<SomeDamnBody>
Alright, well I gotta go to wal mart.
<coventry>
The problem is that I need the existential wrapper A for other reasons, but I don't know how to get at the type of v in "A v" to universalize it.
<pigeonv>
I might be wrong but I think you can't do that since once a value is wrapped, it can't be manipulated (the type is forgotten at runtime)
jbrown has quit [Remote host closed the connection]
<coventry>
Is there any way I can get the detailed signature for that anonymous function, in that context, so that I can lift it out and specify it as a constraint on a named function?
kjak___ has quit [Quit: leaving]
dakk has joined #ocaml
pigeonv_ has joined #ocaml
<coventry>
What should I read to understand what's really going on in the anonymous vs the named function situations there?
pigeonv has quit [Read error: Connection reset by peer]
malina has quit [Read error: Connection reset by peer]
argent_smith1 has quit [Quit: Leaving.]
jao has joined #ocaml
malina has joined #ocaml
<pigeonv_>
the link doesn't work (404)
Denommus has joined #ocaml
<pigeonv_>
a few months ago, I read this article (in French, sorry, but you might have a look at the code) using GADTs to statically type some formulas
<coventry>
Thanks. Line #15 in here has the anonymous function I'm talking about... It's probably because I'm replacing the function parameter with a concrete function. Being able to parameterize it would be very helpful, though: https://pastebin.com/rA7EvNtd
<coventry>
I'll whether google translate and my HS Frence is good enough to piece my way through that. :-)
<pigeonv_>
you can't pass a polymorphic function to another function
<pigeonv_>
I mean, in `let map f l = ...`, `f` is monomorphic
<pigeonv_>
you can't have `val map: ('a. 'a -> 'b) -> 'c list -> 'b list`
<pigeonv_>
we often hear that "only let allows polymorphism"
TheLemonMan has quit [Ping timeout: 240 seconds]
<pigeonv_>
that's related to the way the inference algorithm works
pierpa has joined #ocaml
<pigeonv_>
I had a hard time getting the right "feeling" about it
<coventry>
Yeah, there are a lot of surprises like this. I should probably read the inference algorithm.
<pigeonv_>
sometimes it's better to read a simplified version of it
<pigeonv_>
I probably can't understand the real one
<pigeonv_>
(but I don't consider myself a reference...)
<coventry>
Do you mean just straight Hindley-Milner inference, or a simplified version of the OCaml inference algorithm? If the latter, I'd be grateful for a pointer.
sepp2k has quit [Quit: Leaving.]
<pigeonv_>
the latter. I found Pierre Weiss' book (http://caml.inria.fr/pub/distrib/books/llc.pdf, in French, once again, I'm sorry) easy to follow (it made me finally have a grasp on type inference)
<pigeonv_>
so maybe you could find something equivalent in English
<pigeonv_>
it was sufficient for me so I didn't try the others
<pigeonv_>
"Types and Programming Languages" by Benjamin C. Pierce is great, too
<pigeonv_>
according to a friend who taught me a lot about typing (and wrote a master's thesis in this area), I haven't read it yet so I take his word
_andre has quit [Quit: leaving]
picolino has joined #ocaml
infinity0_ has joined #ocaml
<coventry>
Thanks for all your help, pigeonv_, I'll take a look. I'm finding the chimrod post pretty accessible through Google Translate, so maybe Weiss' book will be too.
infinity0_ has quit [Changing host]
infinity0_ has joined #ocaml
infinity0_ is now known as infinity0
infinity0 has quit [Killed (card.freenode.net (Nickname regained by services))]
<pigeonv_>
oh, that's great news!
<pigeonv_>
I don't know a lot of beginner-friendly material
<pigeonv_>
also
<pigeonv_>
when you have parametrized types,
<pigeonv_>
the compiler often tries to unify them
<pigeonv_>
so, for example, you can't define an 'a t list
<pigeonv_>
a non-empty*
<pigeonv_>
at least, I don't know how to do it without using an existential type
<coventry>
Yep, that's exactly the issue which introduced me to existential types.
<companion_cube>
existential types are nice
<companion_cube>
:)
<pigeonv_>
"both a gift and a curse", I'd say
<pigeonv_>
since you lose some information
<pigeonv_>
and OCaml doesn't allow unsafe cast
<companion_cube>
which is good
<pigeonv_>
yeah, of course ^^
<pigeonv_>
so you have to think a bit beforehand
<pigeonv_>
otherwise, you end up with a lot of opaque boxes
<pigeonv_>
and errors like "type $T can't escape..."
<companion_cube>
these days I'm experimenting with open sum types + record of functions
<companion_cube>
which emulates objects
<pigeonv_>
yeah
<pigeonv_>
this way, you can pass polymorphic functions as arguments
<pigeonv_>
but without a record, it's impossible
<pigeonv_>
(I forgot about it, soooorry)
sam_ has joined #ocaml
pigeonv_ has quit [Read error: Connection reset by peer]
pigeonv_ has joined #ocaml
sam_ has quit [Ping timeout: 248 seconds]
<coventry>
Thanks, the record trick works here, but only with "type monadic_encoding_function = { f: 'a. 'a encoding -> 'a option encoding }"... If I try to do "type monadic_encoding_function = { f: 'a 'b. 'a encoding -> 'b encoding }", it complains that it's too general for the "option: 'a encoding -> 'a option encoding" function. Is there a way to work around that?
<coventry>
(Not your fault, pigeonv_... I should have remembered the record trick. I've seen it before.)
<coventry>
This is what I'm trying to do: https://pastebin.com/Q4fjvan6 . Fails with "This field value has type 'c. 'c Data_encoding.encoding -> 'c option Data_encoding.encoding which is less general than 'a 'b. 'a Data_encoding.encoding -> 'b Data_encoding.encoding"
<coventry>
How does it break things that option is a less general type than the field requires?
kakadu_ has quit [Remote host closed the connection]
<pigeonv_>
I think that 'a. 'b. 'a -> 'b is always too general
<pigeonv_>
if you transpose this to propositions
<pigeonv_>
you get "for all proposition a, for all proposition b, a implies b"
<pigeonv_>
but it's obviously false since if you take a=true, b=false, "true implies false" is false
<pigeonv_>
you can write such a function
<pigeonv_>
but it never terminates gracefully
<pigeonv_>
`fun _ -> failwith "boom"`
<pigeonv_>
actually, `let f _ = failwith "boom"`
<pigeonv_>
yields `val f : 'a -> 'b = <fun>`
<coventry>
Are true and false values, in addition to being bool types?
<pigeonv_>
oh no
<pigeonv_>
actually, there's some kind of relationship between types and propositions
<pigeonv_>
so, you can "convert" a type (e.g. a function type) to a proposition
<pigeonv_>
an arrow becomes an implication
<pigeonv_>
here, I chose simple propositions
<pigeonv_>
(in the usual logic)
<pigeonv_>
to prove that this type doesn't exist (for programs that terminate)
<coventry>
Yeah, I started to read the book on Homotopy Type Theory, a while back.
<coventry>
(Oh, and of course I meant "Are true and false *types*, in addition to being bool *values*?")
<pigeonv_>
not by default ^^
<pigeonv_>
you could define them
<pigeonv_>
and then play with logic at the type level