Shen and exhaustive pattern matching?

[Konstantin Tcholokachvili]

Hello,

I'm wondering if exhaustive pattern matching (like in Standard ML) is featured in Shen.

It sorts out that it's not the case but I want to be sure.

For example I defined a simple function to check this fact:

(14+) (tc +)

(15+) (define logical_and                               

{number --> number --> boolean}

0 _ -> false

1 1 -> true)

logical_and : (number --> (number --> boolean))

In this function the case "1 0" isn't handled but warnings aren't reported.
So is it possible to have warnings in such cases or exhaustive pattern matching?

Don't misunderstand me, I like Shen.

Regards,

Konstantin Tcholokachvili

[Mark Tarver]

Good question. no; its very difficult to perform that in Shen because
the notation is far less restrictive than SML. For example

if (elements X (value *foos*))
________________________
X : foo;

means that exhaustive testing would require the compiler to look in a
global etc. Really its not feasible in general.

Mark

On Nov 2, 11:20 pm, Konstantin Tcholokachvili <tchol...@gmail.com>
wrote:

[JS]

Are there enough useful cases where it is feasible such that the
following would make sense:

1) Try to determine if patterns are exhaustive using feasible
techniques, give warning if it's determined not exhaustive.
2) If #1 was inconclusive, then if there is no wildcard (aka. match
anything) pattern match, give warning.

So that, in the cases where the compiler cannot determine it, it warns
you. Then the programmer can just add a wildcard pattern where needed
and be assured that he always has exhaustive pattern matching.

[Mark Tarver]

This would require meta-reasoning over (not with) sequent calculus
rules. Not easy though some cases can be done, the general case is v.
hard.

Mark

[JS]

Right, that's why I said: just do the feasible stuff for #1, and then
#2 is the fallback. #2 would be trivial to implement, wouldn't it? You
just have to see if there is a pattern that is the arity number of
variables.

Supporting compile time prohibition of partial functions is just as
important as type safety in my opinion when we're considering software
assurance. What's the point of something being type safe if you can
pass in a "safe" value that then blows up because the function is
partial?

> --
> You received this message because you are subscribed to the Google Groups "Qilang" group.
> To post to this group, send email to qil...@googlegroups.com.
> To unsubscribe from this group, send email to qilang+un...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/qilang?hl=en.
>

[Mark Tarver]

It's certainly trivial to detect a potentially partial function and
flag a warning; but #1 will be a messy partial program covering a
limited number of cases. If you want to go in this direction you need
to construct a compiler for ML types into Shen - quite doable - and
then write a metaprogram testing for exhaustive cases.

Mark

[JS]

Why would you need a compiler for ML types?

I didn't think we were discussing having ML types in Shen. Rather just
about exhaustive pattern matching for Shen types.

[Mark Tarver]

As I said, you cannot do this for the range of types Shen can express
using the full resources of the language. You would have to restrict
it to a range of types expressed or expressible in ML style notation.
Probably bar side-conditions.

There is no general elegant solution here.

Mark

[Mark Tarver]

I thought this thread was worth revisiting You asked

"I'm wondering if exhaustive pattern matching (like in Standard ML) is
featured in Shen."

The answer is 'no'

"So is it possible to have warnings in such cases or exhaustive

pattern matching?".

I said there is no general algorithm for testing exhaustive matching
wrt arbitrary Shen type defs *but* you set up your type definitions in
a case based way to do exhaustive testing for you.

For example, here is such a definition of bit.

Shen 2010, copyright (C) 2010 Mark Tarver
www.shenlanguage.org, version 7
running under Common Lisp, implementation: CLisp
port 1.2 ported by Mark Tarver

(0-) (datatype bit

X : bit; P : A; Q : A;
______________________
(cases (= X 1) P
(= X 0) Q) : A;)
bit

(1-) (tc +)
true

(2+) (define logical-and
{bit --> bit --> boolean}
X Y -> (cases (= X 1) (cases (= Y 1) true
(= Y 0) false)
(= X 0) false))
logical-and : (bit --> (bit --> boolean))

You can check that if you miss a case out in that definition that the
whole thing fails. A few remarks.

1. Cases must not only be exhaustive, but have to be entered in the
same order as in the type def.
2. Exhaustive failure is signalled by a type error message.
3. The system has no idea of what a bit is. To armour the system
against possible non-exhaustive error, you want to avoid defining a
bit as a concrete type and instead have your own bit-entry function

(define bit-entry
-> (let Bit (input)
(cases (= Bit 0) Bit
(= Bit 1) Bit
true (error "~A is not a bit~%" Bit))))

and have the axiom

_________________
(bit-entry) : bit;

Mark

[Konstantin Tcholokachvili]

Thank you for the precision.
It's an interesting point.

Konstantin Tcholokachvili

2012/11/8 Mark Tarver <dr.mt...@gmail.com>