Re: [open-axiom-devel] [fricas-devel] Re: What can be done with types as first-class objects?

[Bill P. <bil...@ne...>]

Ok, thanks.

On Fri, Aug 19, 2011 at 6:08 PM, Gabriel Dos Reis <gd...@cs...> wrote:
> | >
> | > )abbrev category MYAGG MyAggegate
> | > MyAggegate(): Category == Type with
> | >    elementType: Ring              -- to be defined by each domain
> | >    toList: % -> List elementType  -- idem
> | >    sumAll: % -> elementType       -- this one has a default implementation
> | >  add
> | >    sumAll x == reduce(_+,toList x,0$elementType)
> | >
> | >
> | > This is just one simple example of (indirect) dependency.
> | > Type dependency requires an advanced decision procedure of type equality
> | > that goes beyond syntactic equally (which is the theoretical
> | > underpinning of most of current Spad, ML, and Haskell98 type system.)
> | >
> |
> Bill Page <bil...@ne...> writes:
> | If the associated type is "defined on case by case basis by each
> | domain" we can make the dependency more explicit. Presumably we still
> | want types to be static. Is there any situation where the following
> | would not be adequate?
>
> The issue is not whether an associated type can be *encoded*.
>
> what you have done is to turn an implicit parameter (existentially
> quantified) into an explicit parameter (universally quantified), and
> ask each user to pass that around all the time, blurring the distinction
> between what is essential parameter from what is derivable (associated
> types).  It becomes unbearable when the number of associated type
> grows or there are redundancies.

Yes you are right. I see the point.

> There are some examples of that in the existing AXIOM algebras --
> and the problem is well know (at least from discussions with
> Stephen Watt.)
>

Yes, I recall such discussions.

> This is a well known technique that has been around for a while.  In fact,
> it was the status quo in Haskell, until the survey [1] that prompted the
> Haskell people to consider associated types, that later evolved into
> type families.   So, you are taking the opposite route of `improvements'
> that we have seen so far :-)  See discussions in the literature below.
>
> [1] http://dl.acm.org/citation.cfm?doid=949305.949317
> [2] http://dl.acm.org/citation.cfm?doid=1086365.1086397
> [3] http://dl.acm.org/citation.cfm?doid=1190315.1190324
> [4] http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf
>

Thanks for the references.

> [...]
>
> | Note: I had some problems using reduce in this context.
>
> what was it?
>

Sorry, thinko. I just forgot the package call. The following compiles:

)abbrev category MYAGG MyAggegate
MyAggegate(ElementType: Ring): Category == Type with
   elementType: Ring        -- to be defined by each domain
   toList: % -> List ElementType  -- idem
   sumAll: % -> ElementType       -- this one has a default implementation
 add
   elementType == ElementType
   sumAll x == reduce(_+,toList x,0)$ListFunctions2(ElementType,ElementType)

--

Here is another example similar to yours except the dependency is only
on a value instead of a type. This compiles: (in OpenAxiom):

--
)abbrev category MYITUP MyIntegerTuple
MyIntegerTuple(): Category == Type with
   elementSize: NonNegativeInteger  -- to be defined by each domain
   toProd: % -> DirectProduct(elementSize,Integer)
   sumAll: % -> Integer  -- this one has a default implementation
 add
   sumAll x == reduce(_+,entries toProd x,0)$ListFunctions2(Integer,Integer)
--

(1) -> )co dep4a-gaby.spad
   Compiling OpenAxiom source code from file /home/page/dep4a-gaby.spad
      using Spad compiler.
   MYITUP abbreviates category MyIntegerTuple

...

(1) -> )sh MYITUP
 MyIntegerTuple  is a category constructor
 Abbreviation for MyIntegerTuple is MYITUP
 This constructor is exposed in this frame.
 Issue )edit /home/page/dep4a-gaby.spad to see algebra source code for MYITUP

------------------------------- Operations --------------------------------
 elementSize : NonNegativeInteger      sumAll : % -> Integer
 toProd : % -> DirectProduct(elementSize,Integer)

However I was unable to find a way to compile a domain using this category. E.g.

--
)abbrev domain MYITUPD MyIntegerTupleDomain
MyIntegerTupleDomain():MyIntegerTuple with
    sample: () -> %
    coerce: % -> OutputForm
  == add
    Rep == DirectProduct(3,Integer)
    elementSize == 3
    toProd(x) == rep x
    sample() == per directProduct( [1,2,3] )
    coerce(x) == (entries rep x)::OutputForm
--

(1) -> )co dep4b-gaby.spad
   Compiling OpenAxiom source code from file /home/page/dep4b-gaby.spad
      using Spad compiler.
   MYITUPD abbreviates domain MyIntegerTupleDomain
------------------------------------------------------------------------
   initializing NRLIB MYITUPD for MyIntegerTupleDomain
   compiling into NRLIB MYITUPD
   Adding $ modemaps
   Adding Integer modemaps
   Adding NonNegativeInteger modemaps
   Adding PositiveInteger modemaps
   Adding Rep modemaps
   compiling exported elementSize : () -> NonNegativeInteger
      MYITUPD;elementSize;Nni;1 is replaced by 3

;;;     ***       |MYITUPD;elementSize;Nni;1| REDEFINED
Time: 0.02 SEC.

   Adding DirectProduct(elementSize,Integer) modemaps
   compiling exported toProd : % -> DirectProduct(elementSize,Integer)
****** comp fails at level 1 with expression: ******
error in function toProd

((|rep| |x|))
****** level 1  ******
$x:= (rep x)
$m:= (DirectProduct elementSize (Integer))
$f:=
((((|x| # #) (|#| # #) (* # # #) (** # # #) ...)))

   >> Apparent user error:
   Cannot coerce x of mode DirectProduct(3,Integer) to mode
DirectProduct(elementSize,Integer)


Regards,
Bill Page.