type declarations & inference in Haskell or ML?

[gusl]

Does Haskell or ML support code like the following?


>> a : p;
a : p

>> b : q;
b : q

>> c : p -> q -> r;
c : p -> q -> r

>> d = (c a);
d : q -> r

>> f : r -> s;
f : r -> s

>> e = lambda(x) (f(d x));
e : q -> s


Note that I get these inferences even though the variables were not instantiated, and the functions were not implemented.

Comments

[simrob.livejournal.com]

You could do it in ML by declaring a signature STUFF and then using a functor that expects a module of type STUFF.

signature STUFF = sig
type p
type q
type r

val a : p
val b : q
val c : p -> q -> r
val d : q -> r
val f : r -> s
end

functor Funct(X: STUFF) = struct
open X
val e : fn x => f(d x)
end

[simrob.livejournal.com]

That last one should have been val e = fn x => f(d x) - I'm sure there were other errors too :)

[gustavolacerda.livejournal.com]

after I enter STUFF, do I need ";;"? If so, then I get an error: "Unbound constructor STUFF".

[simrob.livejournal.com]

Okay, let's do this right:

signature STUFF = sig
type p
type q
type r
type s

val a : p
val b : q
val c : p -> q -> r
val d : q -> r
val f : r -> s
end

functor Funct(X: STUFF) = struct
open X
val e = fn x => f(d x)
end;;

If you put that into the REPL loop you should get what you're looking for. Or you can put it, without the ;;, into "foo.sml" and then say use "foo.sml";; from inside the REPL loop. This is SML, not OCaml, by the way.

[gustavolacerda.livejournal.com]

I only have OCaml. Does this become a lot different?

[roseandsigil.livejournal.com]

module type STUFF = sig
type p
type q
type r
type s

val a : p
val b : q
val c : p -> q -> r
val d : q -> r
val f : r -> s
end

module Funct(X: STUFF) = struct
include X
let e = fun x -> f(d x)
end;;

[gustavolacerda.livejournal.com]

Thanks! That works!

if I now want to instantiate/implement some of these variables/functions, would I use the constructor STUFF, passing in p,q,r,etc? What if I only want to instantiate some of them?

[ikeepaleopard]

If you don't want to deal with modules, you can give non-terminating terms or exception raising terms any type you want e.g.

let a = (raise Fail) : p

[simrob.livejournal.com]

Also true. Can't really do that inside the REPL loop, though.