SPAD Syntax Issues

This is one of a set of pages about the Axiom CAS and its forks, particularly FriCAS, these pages start here. This particular page dicusses the issues in designing a syntax to appriximate SPAD.

Expressions and Type Expressions

There is an issue about whether we have seperate rules for expressions and type expressions or do we recognise both with the same set of rules?

By 'expression' I mean somthing like: 2+(3*6) although expressions may be a lot more complicated than this and may include variables, functions and instances of more complicated types.

By 'type expression' I mean somthing like:

Record(minXVal : SF, maxXVal : SF)  

A type expression may also be a lot more complicated than this and contain Records, Unions, functions and so on.

The problem is that the distiction between types and values is not clear from the syntax alone. Since we have constructs like dependent types and type constuctors then a given expression may have a mixture of values and types. Since SPAD uses type inference we would possibly have to trace back through several lines to determine if a given element is types or value. That is, the only way to know would be to analyse the semantics rather than the syntax.

For example, is the right hand side of this assignment a type or a value?

Eu := CliffordAlgebra(3,Fraction(Integer),[[1,0,0],[0,1,0],[0,0,1]])

The only way to know would be to check though other code to find out if 'CliffordAlgebra' is a type constuctor or an ordenary function or, alternativly see what 'Eu' is used for. It turns out 'Eu' is a type:

e1:Eu := e(1)

The parser can't do this type of checking and therefore we cant really distinguish, at the syntax level, between types and values.

Therefore, at the syntax level, I think there should be no distinction between 'expressions' and 'type expressions', just 'expressions' which could be either type.

However, I have not yet managed to do this, in the current syntax, without ambiguaties that I can't resolve. This means that the current syntax does have some rules that are specific to 'type expressions' and some messy complication to try to get round these issues. I need to do more work to sort this out.





metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.