Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Haskabelle configuration

view this post on Zulip Email Gateway (Aug 18 2022 at 19:16):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Haskabelle developers,

I am trying to import some Haskell code using Haskabelle for Isabelle2011-1. So
far, I ran into the following two problems:

  1. Bound variable names clash with previous constant names.
    For example, in the following Haskell program

f = \x -> x
g = f
h f = (f, g)

f is bound in h's definition, but also defined previously.

Haskabelle generates the following definitions in Isabelle:

definition f where "f = (% x . x)"
definition g where "g = f"
fun h where "h f = (f, g)"

Obviously, this is not what I want, because h's definition now "pattern-matches"
on the constant f, but it should actually be as follows:

fun h where "!!f. h f = (f, g)"

The same problem also occurs with predefined constants from the Isabelle
library. I suggest that Haskabelle explicitly adds the universal quantification
to all bound variables that occur on the left-hand equation of a function
definition such that it need not know which names are used.

Is there some other way than manually renaming all such variables in the Haskell
code? This is something I actually want to avoid.

  1. do notation
    Apparently, Haskabelle has some undocumented support for do notation and monads.
    At least, this is what I gather from the files in ex/ and the error message for
    the following program:

f = do {
x <- [1,2];
y <- [x + 1];
[y]
}

haskabelle_bin: Do syntax is used without sufficient type information!

What type information do I have to add (and where) such that such examples
compile? Actually, I would have expected that no type information were
necessary, because Isabelle's parser setup for do notation in
Library/Monad_Syntax should resolve the operations correctly.
Can I configure Haskabelle to use that setup?

Thanks for any help,
Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 19:17):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

maybe Gerwin can point you to some reference – that do-notation
extension was developed at NICTA, AFAIR.

Florian

Last updated: Nov 21 2024 at 12:39 UTC