sz0 has quit [Quit: Connection closed for inactivity]
muelleme has quit [Ping timeout: 240 seconds]
govg has joined #ocaml
silver has joined #ocaml
jnavila has joined #ocaml
gtrak_1 has joined #ocaml
gtrak has quit [Ping timeout: 264 seconds]
TarVanimelde has joined #ocaml
pierpal has quit [Ping timeout: 264 seconds]
bartholin has joined #ocaml
muelleme has joined #ocaml
shinnya has joined #ocaml
mfp has joined #ocaml
TarVanimelde has quit [Quit: TarVanimelde]
slash^ has joined #ocaml
muelleme has quit [Ping timeout: 240 seconds]
Kalpatitoo has quit [Ping timeout: 276 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 256 seconds]
silver has quit [Read error: Connection reset by peer]
FreeBirdLjj has joined #ocaml
pierpal has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 264 seconds]
pierpal has quit [Ping timeout: 245 seconds]
jao has joined #ocaml
jao has quit [Disconnected by services]
jao has joined #ocaml
Haudegen has joined #ocaml
Kalpatitoo has joined #ocaml
<Drup>
Kalpatitoo: you just give names to your libraries and use that in your tests and that's it.
sh0t has joined #ocaml
FareTower has quit [Ping timeout: 264 seconds]
jao has quit [Ping timeout: 256 seconds]
slash^ has quit [Quit: Leaving]
slash^ has joined #ocaml
<bartholin>
How do I convert an ADT structure to the corresponding GADT structure? My head hurts, so I wrote an example and it does not work: https://p.teknik.io/f1v6O
<Drup>
Do you understand why it doesn't work ?
FreeBirdLjj has joined #ocaml
<bartholin>
Drup: typechecking fails
<Drup>
Obviously :)
<bartholin>
I believe I should "typecheck" the input myself, but I don't know how to say "if the recursive call returns an incorrect type, then throw an exception"
<Drup>
right, so that's the correct intuition
<Drup>
you will first need a function that, given a gast, gives you back the type
<bartholin>
Do I have to reify types?
<Drup>
yes
muelleme has joined #ocaml
mengu has joined #ocaml
<bartholin>
but how do I denote my reification of types?
mengu has quit [Client Quit]
<Drup>
something like `type 'a ty = int TyInt | bool TyBool` and a function `infer_type : 'a gast -> 'a ty`
<bartholin>
oooooh
<Drup>
This way, when you pattern match on the ty, you get information about the gast's type variable
<bartholin>
ooooooooooooooooooooh
<Drup>
err, TyIng : int ty | TyBool : bool ty
Bronsa` has joined #ocaml
<bartholin>
wait
<bartholin>
how does it help me to know the type of the ADT structure
<Drup>
well, then you can do something like this : `If (b, e1, e2) -> let b' = ast_to_gast b in match infer_type b' with | Int -> failwith "NOPE" | Bool -> .....`
<Drup>
TyInt*
<bartholin>
oh
<bartholin>
ok
<Drup>
As you said, you typecheck your entry :)
<bartholin>
What is the correct type decoration of ast_to_gast? I tried ast_to_gast : type a. ast -> a gast and ast_to_gast : ast -> (type a. a gast), but it does not work
Soni has quit [Ping timeout: 265 seconds]
<Drup>
`type a. a ast -> a gast`
Soni has joined #ocaml
tarptaeya has joined #ocaml
<bartholin>
does not work
<bartholin>
let rec ast_to_gast : type a. ast -> a gast = function
<bartholin>
| _ -> assert false
<bartholin>
| Int i -> Int' i
<bartholin>
| Bool b -> Bool' b
<bartholin>
Error: This expression has type bool gast
<bartholin>
Type bool is not compatible with type a
<bartholin>
but an expression was expected of type a gast
Kalpatitoo has quit [Ping timeout: 264 seconds]
FreeBirdLjj has quit [Ping timeout: 260 seconds]
<octachron>
bartholin, you cannot produce a naked gast from ast: it is impossible to synthetize static type information from a dynamical value
<Drup>
oh, right, you need to fix the type of the toplevel thing
<bartholin>
octachron: is Drup trolling me?
<Drup>
nope, just being slightly distracted
<octachron>
bartholin, no. Reifing the type is one solution: you can define a function "ast -> 'a ty -> 'a gast option"
<octachron>
that fails if the type of the constructed (g)ast is not compativle with 'a ty.
<bartholin>
oh ok
<bartholin>
so I can do dynamical "type checking", but no dynamical "type inference".
<Drup>
You can .... for the inner nodes
<octachron>
you can do dynamical type inference, but you cannot lift it to the static level
dtornabene has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
sh0t has quit [Ping timeout: 256 seconds]
gareppa has joined #ocaml
<bartholin>
Now it works, but I am not very happy with the Eq case, because I have to check all possible types, as I don't have type inference https://p.teknik.io/H7lJW
barcabuona has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
<thizanne>
bartholin: your solution actually implements some kind of inference, the algorithm being "I can know the type by looking at the ast variant. When I'm on a parameter of Eq, I try Int and if it's not int then it should be bool"
<thizanne>
you can push this one level farther and, when looking at the first parameter of Eq, look at the "root variant" to know what type it should be (and the second parameter should have the same type)
<thizanne>
(for instance by having a type not_gadt_type = Int | Bool)
<octachron>
another option is to implement inheritance with a type "dyn_ast = Dyn: 'a gast * 'a ty -> dyn_ast" and a function "ast -> dyn_ast"
<octachron>
then type checking can be done with a function "'a ty -> 'b ty -> ('a,'b) eq option"
jnavila has quit [Ping timeout: 240 seconds]
Bronsa` has quit [Ping timeout: 268 seconds]
<thizanne>
I like this one
<thizanne>
bad algebra make me think that you compose an universal gadt with an existential one so you get something close enough to a classical abstract type to be able to write the inference with this type
shinnya has quit [Ping timeout: 260 seconds]
sh0t has joined #ocaml
muelleme has quit [Ping timeout: 260 seconds]
muelleme has joined #ocaml
sh0t has quit [Remote host closed the connection]
sh0t has joined #ocaml
muelleme has quit [Ping timeout: 240 seconds]
kotrcka has joined #ocaml
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
zpe has quit [Ping timeout: 264 seconds]
jjmeyer0 has joined #ocaml
gareppa has quit [Quit: Leaving]
jbrown has joined #ocaml
zpe has joined #ocaml
FareTower has joined #ocaml
zpe has quit [Remote host closed the connection]
kotrcka has left #ocaml [#ocaml]
ziyourenxiang has quit [Ping timeout: 260 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
jao has joined #ocaml
Kalpatitoo has joined #ocaml
jnavila has joined #ocaml
Haudegen has quit [Remote host closed the connection]
tormen_ has quit [Quit: Lost terminal]
jnavila has quit [Ping timeout: 245 seconds]
Haudegen has joined #ocaml
jnavila has joined #ocaml
<sh0t>
what's a standard way to generate fresh names (strings)?
<Drup>
sh0t: `let f = let r = ref 0 in () -> incr r ; Format.sprintf "name%i" !r`
<companion_cube>
✔
<companion_cube>
forgot a `fun` before the `()` tho
<Drup>
modulo syntax, yes :p
jnavila has quit [Ping timeout: 240 seconds]
<sh0t>
Drup thanks! thats cool!
<sh0t>
companion_cube, thatnks for the syntax check
FareTower has quit [Ping timeout: 240 seconds]
FareTower has joined #ocaml
Bronsa` has joined #ocaml
<bartholin>
What does Error: Unexpected existential mean?
<companion_cube>
that's pretty fishy, don't think I ever got that
<Drup>
bartholin: does your life has meaning ?
<Drup>
Why are you getting up in the morning ?
<Drup>
What will you do in 20 years ?
<companion_cube>
:D
<bartholin>
D:
<companion_cube>
thank $deity that ocamlc is not asking me that
<Drup>
I'm pretty sure I made that joke already
<Drup>
bartholin: can you pastebin the code that produces it ?
<bartholin>
I am playing with GADTs, and I tried to extract something with a "non-static" type.
<bartholin>
https://p.teknik.io/OY6RL I have a function foo : string -> dyn', that converts a string to a (_,_,_) format (for printf). I only deal with "%d" because I am testing.
<octachron>
bartholin, just to be sure, you are aware of the existence of Scanf.format_from_string?
<octachron>
Anyway, the error message that you got is expected because you cannot expose an existenlly quantified type at the toplevel
<octachron>
This is mostly the idea that you compute a (static) type from a (runtime) value
<bartholin>
ok
jnavila has joined #ocaml
<octachron>
(even if the error message could be improved, in its current state it reads a bit as "you know that I cannot let do that" )
slash^ has quit [Quit: Leaving]
<Drup>
octachron: it should be a message of the form "<thing> will escape", shouldn't it ?
sz0 has joined #ocaml
<companion_cube>
I'm sorry Dave, I'm afraid I can't let this type escape
<octachron>
Drup, yes; maybe a bit more specific but it should mention the corresponding existential types and focuses on the expectations of users and not typechecker implementaters
jnavila has quit [Remote host closed the connection]
jimmyrcom has joined #ocaml
FareTower has quit [Ping timeout: 240 seconds]
FareTower has joined #ocaml
gareppa has joined #ocaml
gareppa has quit [Quit: Leaving]
zpe has joined #ocaml
FareTower has quit [Ping timeout: 240 seconds]
argent_smith has quit [Quit: Leaving.]
zolk3ri has quit [Quit: leaving]
<bartholin>
oh
<bartholin>
I have a simpler example.
<bartholin>
type foo = Foo : 'a -> foo
<bartholin>
Error: Unexpected existential
<bartholin>
let Foo y = let x = Foo 3 in x;;
<octachron>
bartholin, what type would you expect for y?
<mrvn>
octachron: 'a
<mrvn>
bartholin: you need a witness type to make any use of the existential
<octachron>
mrvn, and the poor existential quantification?
<octachron>
mrvn, your description is a bit restrictive: "type t = Any_list :'a list -> any_list let len (Any_list l) = List.length l"
tarptaeya has quit [Ping timeout: 276 seconds]
<mrvn>
octachron: Error: Unbound type constructor any_list
<mrvn>
I think you mean "t"
sz0 has quit [Quit: Connection closed for inactivity]
pierpa has joined #ocaml
<octachron>
mrvn, yes or "type any_list = .."
gtrak_1 has quit [Ping timeout: 276 seconds]
gtrak_1 has joined #ocaml
tarptaeya has joined #ocaml
Cale has quit [Read error: Connection reset by peer]
tarptaeya has quit [Quit: Byeeeeeee!]
pierpal has quit [Ping timeout: 245 seconds]
pzp has joined #ocaml
sheijk has joined #ocaml
jimmyrcom has quit [Ping timeout: 264 seconds]
jimmyrcom has joined #ocaml
spew has joined #ocaml
spew has quit [Ping timeout: 256 seconds]
JeanMax has joined #ocaml
JeanMax has left #ocaml [#ocaml]
spew has joined #ocaml
Haudegen has quit [Remote host closed the connection]
silver has joined #ocaml
jimmyrcom_ has joined #ocaml
Kalpatitoo has quit [Read error: Connection reset by peer]