caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* Polymorphic variants question
@ 2006-09-01 17:31 David Allsopp
  2006-09-01 18:33 ` Chris King
                   ` (3 more replies)
  0 siblings, 4 replies; 18+ messages in thread
From: David Allsopp @ 2006-09-01 17:31 UTC (permalink / raw)
  To: OCaml List

Forgive the potentially obvious question --- I'm not very familiar with
polymorphic variants but I think that they're what I want in this situation!

Suppose I'm dealing with three constructors `A, `B and `C and I have a
function f that's supposed to take either `A or `C and return any of `A, `B
or `C. If I write:

let f x = if x = `A then (true, `B) else (false, x)

then I get the type

val f : ([> `A | `B] as 'a) -> bool * 'a

Now, if I try to constrain it to what I'm after with

let (f : [`A | `C] -> bool * [`A | `B | `C]) = fun x -> ...

then I get a type error unless I change
	(false, x)
to
	(false, id x)
with 
	let id = function `A -> `A | `C -> `C

Is there a better way of writing this? I'm using this in the context of
several interrelated lexers where `A, `B and `C are high-level states and
certain lexers can only be called in a subset of those states but each lexer
may yield any value for the next-state. I'd quite like to eliminate the id x
bit since it's only there to "separate" x from the return value for the
type-checker.

Thanks!


David


^ permalink raw reply	[flat|nested] 18+ messages in thread
* Polymorphic variants question
@ 2000-04-26  0:25 Brian Rogoff
  2000-04-26  9:34 ` Jacques Garrigue
  0 siblings, 1 reply; 18+ messages in thread
From: Brian Rogoff @ 2000-04-26  0:25 UTC (permalink / raw)
  To: caml-list

Hi,

A long time ago John Prevost posted a nice trick to get a kind of 
downcasting in OCaml

class type ['a] super =
  object
    method downcast : 'a
  end;;

class type ['a] a =
  object
    inherit ['a] super
    method do_a : int
  end;;

class type ['a] b =
  object
    inherit ['a] super
    method do_b : float
  end;;

type objsum = A of objsum a | B of objsum b;; 

Which have types 

#   class type ['a] super = object method downcast : 'a end
#   class type ['a] a = object method do_a : int method downcast : 'a end
#   class type ['a] b = object method do_b : float method downcast : 'a
end
#   type objsum = A of objsum a | B of objsum b

And to show that it works, he gave the following test code:

class test_a =
    object (s)
      method downcast = A (s :> objsum a)
      method do_a = 1
    end;;
  class test_b =
    object (s)
      method downcast = B (s :> objsum b)
      method do_b = 1.0
    end;;

#  class test_a : object method do_a : int method downcast : objsum end
#  class test_b : object method do_b : float method downcast : objsum end

and so on, testing that this meets assumptions. 

If we replace the variant with a polymorphic variant. 
type objsum = [`A of objsum a | `B of objsum b];;

and then we do the same thing as before the type checker complains. 

# class test_a =
    object (s)
      method downcast = `A (s :> objsum a)
      method do_a = 1
    end;;
# Characters 6-103:
# Some type variables are unbound in this type:
# class test_a : object method do_a : int method downcast : #objsum[>`A]
end
# The method downcast has type #objsum[>`A] where 'a is unbound

This is a good error message, and it tells me what to do to fix the
problem right away: I add an annotation to constrain that "#objsum[>`A]" 

# class test_a =
  object (s)
    method downcast : objsum = `A (s :> objsum a)
    method do_a = 1
  end;;
  class test_b =
    object (s)
      method downcast : objsum = `B (s :> objsum b)
      method do_b = 1.0
    end;;

# class test_a : object method do_a : int method downcast : objsum end
# class test_b : object method do_b : float method downcast : objsum end

Now, in order to avoid surprises in the future, can someone tell me why I
should have expected that type "#objsum[>`A]" to be computed, and hence known
that I would need to constrain the type? It makes sense, but I don't yet
have a good mental model for the typing of polymorphic variants
which would have allowed me to write the correct version immediately. How 
do the experts go about mentally inferring the right types in cases like
this?

-- Brian







^ permalink raw reply	[flat|nested] 18+ messages in thread
end of thread, other threads:[~2006-09-03 23:19 UTC | newest]

Thread overview: 18+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2006-09-01 17:31 Polymorphic variants question David Allsopp
2006-09-01 18:33 ` Chris King
2006-09-01 19:00   ` [Caml-list] " skaller
2006-09-01 19:57     ` David Allsopp
2006-09-01 20:40       ` Jacques Carette
2006-09-01 18:40 ` [Caml-list] " Olivier Andrieu
2006-09-01 19:26 ` Jon Harrop
2006-09-01 19:29 ` skaller
2006-09-01 20:49   ` Andres Varon
2006-09-02 11:16     ` Jacques Garrigue
2006-09-03  1:22       ` Andres Varon
2006-09-03  9:08         ` Jacques Garrigue
2006-09-03 15:00           ` Andres Varon
2006-09-03 23:18             ` Jacques Garrigue
2006-09-03  0:48   ` [Caml-list] Polymorphic variants problem skaller
2006-09-03  1:12     ` Andres Varon
  -- strict thread matches above, loose matches on Subject: below --
2000-04-26  0:25 Polymorphic variants question Brian Rogoff
2000-04-26  9:34 ` Jacques Garrigue

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).