TA Allocation: Use-case for Ampersand version 4?

[WolframKahl]

The interface a certain administrator uses for allocation of teaching assistants (TAs) is a collection of Excel spreadsheets ─ mainly:

• one list of courses, where for each course there is the number of TA positions assigned to the course, and the list of TA candidates the instructor prefers, and where the assigned TAs will be entered.

• one list of student preferences, where each student declares a list of courses they'd prefer to be TA for, and where the courses assigned to that student will be entered.

The sequence structure is relevant since it encodes preference, even though preference is currently not yet referenced in any of the rules below. However, this sequence structure needs to be easily visible in the interface.

Students also have a number of guaranteed TA positions (zero, one, or two), and the initial phase of the assignment will allocate only those guaranteed positions (which are fewer than needed for all courses).

The final assignment will assign TAs to all positions.

The problem with the spreadsheets is that the same relation, CourseTA, is represented twice, as CourseTAList and as TACourseList (names used below), and Excel does nothing to keep these consistent.

Doesn't this sound like a nice use case for Ampersand? I initially thought so, but then I noticed that I had no idea how to do it appropriately, and I even strongly suspect that it cannot yet be done nicely.

Below is a sketch of how I might attempt to do at least the core specification of this nicely in a future version of Ampersand.

I am freely inventing notation that is not too far from current Ampersand notation, and I hope that it is understandable from a current Ampersand background.

CONTEXT AllocateGraduateTAs IN ENGLISH LATEX
  META "author" "Wolfram Kahl"

  CONCEPT Course "Unique identifier for course for purpose of TA allocation"
  CONCEPT GradStud "Graduate Student"

  FUNCTION GuaranteedTAs : GradStud -> Nat  [TOT]
  -- Instead of |Nat|, this could be theoretically {0, 1, 2, 3, 4}, practically {0, 1, 2}
  PRAGMA "" " is guaranteed " " TA positions per year"

  CONCEPT Term = { Term1, Term2, Term3 }
  RELATION IsAvailableFor : GradStud <-> Term

  FUNCTION HeldIn : Course -> Term [TOT]
  
  FUNCTION StudWants : GradStud -> Seq Course [TOT]

  FUNCTION CourseAllocation : Course -> Nat [TOT]
  -- we currently have at least one course with 5 graduate TAs allocated.

  FUNCTION InstructorWants : Course -> Seq GradStud [TOT]

  CONCEPT Phase = { Initial , Final }

  FUNCTION phase : () -> Phase [TOT]

  FUNCTION CourseTAList : Course -> InjSeq GradStud [TOT]
  RELATION CourseTA : Course <-> GradStud
  RULE CourseTA-view : CourseTA = CourseTAList ; elemSeq ~

  -- CourseTAList is the main interface the administrator uses to interact with CourseTA;
  -- the sequence of students in each list typically reflects the confidence in
  -- or urgency of their assignment to this course.

  -- The view CourseTA is what will be published.

  -- Can the interaction with CourseTAList be achieved already now?
  -- If no, how could it be specified?

  RELATION TACourseList : GradStud -> InjSeq Course
  RULE TACourseList-def = CourseTA = elemSeq ; TACourseList ~

  -- TACourseList is a secondary interface for the administrator to interact with CourseTA.
  -- Additions done via CourseTAList would be appended at the end to the entry for that
  -- student in TACourseList.
  -- Similarly, additions done via TACourseList would go to the end of the course entry in CourseTAList.

  RULE FeasibleAlloc : CourseTAList ; seqLength <= CourseAllocation ; natGEq
  PURPOSE RULE "FeasibleAlloc" "Each coures has at most the TAs it needs."

  RULE FinalAlloc : phase = {(_, Final)}
    => CourseTAList ; seqLength = CourseAllocation
    && TACourseList ; seqLength <= GuaranteedTAs ; natGEq
  PURPOSE RULE "FinalAlloc" "Every course has all the TAs it needs, and each graduate student has at least their guaranteed positions."

  RULE InitialAlloc : phase = {(_, Initial)}
    => TACourseList ; seqLength = GuaranteedTAs

  -- The following “rules” are not strict, but the administrator wants to see violations,
  -- so they can be minimised and distributed “fairly”:

  RULE [Warning: color=orange] InstructorHappy : CourseTA <= InstructorWants ; seqElem ~
  RULE [Warning: color=red]    StudentHappy    : CourseTA <= seqElem ; StudWants ~
  RULE [Warning: color=yellow] NoExtraTAs      : TACourseList ; seqLength <= GuaranteedTAs ; natGEq

[RieksJ]

Nice idea. How such an application would currently be done is a bit of a tricky question, because doing an application - even if it is 'just a demo' - that you want to really use is quite different from showing that you can do the basics. For example, if you would like different people to use the application in such a way that they would only be seeing what is of interest to them, you would need some basic functionality from the SIAM (Sessions, Identity and Access Management) module. Also, if you want to have different views for different roles, sorting out the various INTERFACEs may not be trivial. But we've done quite a few demo apps, and this one does not seem to be impossible.

However, it does need some careful crafting, as we don't have the stuff you use in Ampersand. However, we do have sequence-functionality in the Sequences module that you can find in the application repo. Still, it would be a bit cumbersome. To give you an idea, here is how I think what your line FUNCTION InstructorWants : Course -> Seq GradStud might look like when using this module:

CLASSIFY GradStudSequence ISA Sequence

RELATION instructorWants :: Course * GradStudSequence [INJ,UNI,TOT]

ROLE ExecEngine MAINTAINS "Ensure every Course has a GradStudSequence"
RULE "Ensure every Course has a GradStudSequence":  I |- instructorWants;instructorWants~
VIOLATION (TXT "{EX} InsAtom;GradStudSequence
          ,TXT "{EX} InsPair;Course;", SRC I, TXT ";GradStudSequence;_NEW"
          )

Then, work continues to accomodate the insertion and deletion of items the sequence (examples of which are given in the sequences-module, file SeqInterfacing.svc)

[stefjoosten]

@WolframKahl
About your language proposals, I have 10 comments/questions. Perhaps you have answers to my questions. And you might rebound on my comments if you feel like it....

1. The 'FUNCTION' statement is easy. That is syntactic sugar on top of 'RELATION'.
2. The CONCEPT statement with an enumeration is eaqually easy. Neat idea!
3. I don't understand 'FUNCTION CourseTAList : Course -> InjSeq GradStud' , especially the 'InjSeq' bit. Is it some kind of constructor? What is its semantics?
4. 'elemSeq' is not declared. What does it mean? Is it predefined?
5. 'FUNCTION phase : () -> Phase' needs some explanation. Does it have different values over time? If yes, can we still guarantee Leibniz' property?
6. How can a relation be an Interface? (e.g. "TACourseList is a secondary interface for the administrator")
7. ' [Warning: color=orange]' is an annotation for the presentation layer (i.e. CSS). We have some of that already, but a systematic, attractive, and easy way to do this is what we need. For now i have postponed this question for later. But maybe later is now?
8. What is the meaning of '<=' in 'RULE FeasibleAlloc'? It seems that it has type 'Course*Nat' How does the compiler know? What does it mean?
9. Splitting a rule in partial rules with conditions ( as in 'FinalAlloc' and 'InitialAlloc' is attractive. Shouldn't be hard...
10. Anything I missed out on?

[stefjoosten]

@WolframKahl Do you have examples of the two spreadsheets you mentioned above? Would you care to share them?