Poly/ML January 2016

polyml@lists.polyml.org

11 participants
14 discussions

Type inference issue using signature constraint
by phil.clayton＠lineone.net 12 Jan '16

12 Jan '16

I have an example where a module is type checking fine even though I have introduced a type error into it! I've reduced it down to a small example. It looks like there is a problem using type constraints from a signature where the signature is also required to resolve record components. See attached example for details. Phil

1 0

addPrettyPrinter type security
by rda＠lemma-one.com 11 Jan '16

11 Jan '16

PolyML.addPrettyPrinter checks its printArgTypes parameter carefully when you are installing a pretty-printer for a polymorphic type. As far as I can see it guarantees type security for polymorphic types. However, when you install a pretty-printer for a monomorphic type, the parameter isn't checked at all. E.g., the following code doesn't result in any error messages and ends by crashing poly. datatype MONO = Mono of int; fun pp_mono1 _ (i : int) (Mono j) = ( PolyML.PrettyString (Int.toString (i + j)) ); PolyML.addPrettyPrinter pp_mono1; Mono 42; (* Prints "val it = 42: MONO" - apparently i was 0 *) fun pp_mono2 _ (r : int ref) (Mono _) = ( PolyML.PrettyString (Int.toString (!r)) ); PolyML.addPrettyPrinter pp_mono2; Mono 42; (* Crashes *) Shouldn't processArgTypes be required to have type unit when defining a pretty-printer for a monotype? The patch below implements this check and tries to improve the error message (which is already a bit misleading if you get something wrong for a type with more than one parameter). Regards, Rob. diff --git a/mlsource/MLCompiler/VALUE_OPS.ML b/mlsource/MLCompiler/VALUE_OPS.ML index 1535d4f..9e00f0d 100644 --- a/mlsource/MLCompiler/VALUE_OPS.ML +++ b/mlsource/MLCompiler/VALUE_OPS.ML @@ -958,8 +958,8 @@ struct val typeVars = List.tabulate(arity, fn _ => mkTypeVar (0, false, true, false)) val tupleType = case typeVars of - [] => (* No arg so we can have anything here. *) - mkTypeVar (generalisable, false, false, false) + [] => (* No arg so must have unit. *) + unitType | [arg] => mkFn arg (* Just a single function. *) | args => mkProductType(List.map mkFn args) val addPPType = mkFunctionType(argPrints, mkFunctionType(installType, pretty)) @@ -970,7 +970,7 @@ struct in checkPPType(addPPType, testType, "addPrettyPrint", lex, loc, fn () => - PrettyString "addPrettyPrint element functions must have type 'a * int -> pretty") + PrettyString "addPrettyPrint element functions must have type 'a * int -> pretty, 'b * int -> pretty, ... with one function for each type parameter") end; (* Only report the error when the function is run. Because addPrettyPrint is

2 1

Towards Poly/ML 5.6
by David.Matthews＠prolingua.co.uk 09 Jan '16

09 Jan '16

I've updated the github repository with pre-built compilers for 5.6 Release. This is now the release candidate. Unless there are any significant problems this will be released in the next few weeks. Best wishes for 2016, David

8 18

5.6 failures on OSX
by Michael.Norrish＠nicta.com.au 08 Jan '16

08 Jan '16

Our regression testing from poly's master branch with sources that are fine on 5.5.2 is showing repeated "random" failures on OSX. You can see the build history at https://travis-ci.org/HOL-Theorem-Prover/HOL/builds (ignore the k11-release-prep branch failures). In all of the recent failures of HOL's master, you'll see that it is the "GITPOLY" build on OSX failing. The GITPOLY build on Linux is fine. Unfortunately, the failures are happening at different times in the build. The only thing they seem to have in common is that there is a test (using OS.Process.isSuccess) of the result of another execution ultimately set up with OS.Process.system. The output even somewhat suggests that the child process terminated successfully; could it be that the return code is being randomly mis-interpreted? Michael ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 2

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML January 2016