[Caml-list] isn't this cheating?

[Caml-list] isn't this cheating?

[Gerd Stolpmann]

[-- Attachment #1: Type: text/plain, Size: 1508 bytes --]

Hi,

just fixing up some GADT code. I came across this:

I have a module M with module type T:

module type T = sig
  type p
  val p_type : p Ztypes.ztype
  val output : float -> p
end

Now, Ztypes.ztype is a GADT like

type _ ztype =
  | Zstring : string ztype
  | Zfloat : float ztype
  | ...

In a function calling M.output I cannot assume that p=float unless I
check it explicitly. So I wrote

let f() =
  let m_output =
    match M.p_type with
      | Ztypes.Zfloat -> (M.output : float -> float)
      | _ -> assert false in
 ...

This doesn't type-check. Funnily, you can fix it by simply adding a
newtype to the function:

let f : type t = fun() ->
  let m_output =
    match M.p_type with
      |
Ztypes.Zfloat -> (M.output : float -> float)
      | _ -> assert false
in
 ...

It is just the presence of t that makes it type-check. This type is not in any way bound to the type parameter of ztype, and this is somewhat unexpected. From a user's perspective it is very comfy that the newtype works like a configuration switch for the type checker. Nevertheless, I wonder why it is like that.

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

Re: [Caml-list] isn't this cheating?

[Gerd Stolpmann]

[-- Attachment #1: Type: text/plain, Size: 1707 bytes --]

Forget this message.

Gerd

Am Freitag, den 26.08.2016, 00:33 +0200 schrieb Gerd Stolpmann:
> Hi,
> 
> just fixing up some GADT code. I came across this:
> 
> I have a module M with module type T:
> 
> module type T = sig
>   type p
>   val p_type : p Ztypes.ztype
>   val output : float -> p
> end
> 
> Now, Ztypes.ztype is a GADT like
> 
> type _ ztype =
>   | Zstring : string ztype
>   | Zfloat : float ztype
>   | ...
> 
> In a function calling M.output I cannot assume that p=float unless I
> check it explicitly. So I wrote
> 
> let f() =
>   let m_output =
>     match M.p_type with
>       | Ztypes.Zfloat -> (M.output : float -> float)
>       | _ -> assert false in
>  ...
> 
> This doesn't type-check. Funnily, you can fix it by simply adding a
> newtype to the function:
> 
> let f : type t = fun() ->
>   let m_output =
>     match M.p_type with
>       |
> Ztypes.Zfloat -> (M.output : float -> float)
>       | _ -> assert false
> in
>  ...
> 
> It is just the presence of t that makes it type-check. This type is
> not in any way bound to the type parameter of ztype, and this is
> somewhat unexpected. From a user's perspective it is very comfy that
> the newtype works like a configuration switch for the type checker.
> Nevertheless, I wonder why it is like that.
> 
> Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------



[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]