Re: [isabelle] Solving a type class constraint



Am 04.06.2014 10:42, schrieb Lars Hupel:
Hello,

I'm trying to produce well-sorted terms in Isabelle/ML. Basically, I have a predicate "P" of type "'a" with some sort constraint, and I want to apply it to some polymorphic constant. Consider this small Isar snippet:

class foo
consts
  P :: "'a::foo ⇒ bool"
  opt :: "'a option"

instantiation option :: (foo) foo
begin
  instance ..
end

declare [[show_sorts]]

ML_val{* @{term "P opt"} *}

As is obvious from the output, type inference instantiates P's type to

  'a∷foo option ⇒ bool

The important bit here is that it slapped a "foo" constraint on the type variable.

However, it is not obvious to me how to do the same thing in ML. I mean, it's trivial to construct a well-typed term for "P opt":

ML{*
  fun mk_P t = Const (@{const_name P}, fastype_of t --> @{typ bool}) $ t;
  val t = mk_P @{term opt};
  val ct = cterm_of @{theory} t;
*}

Sounds to me like you just would want to use the type inference itself:

ML{*
fun mk_P t = Const (@{const_name P}, dummyT) $ t |> Syntax.check_term @{context};
  val t = mk_P (Const (@{const_name opt}, dummyT));
  val ct = cterm_of @{theory} t;
*}

You can refine the "dummyT"s if the type that you get is too general.

Hope that helps,
Dmitriy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.