induction datatype + dependent type = logic programming + named clause - query

[xieyuheng]

logic programming + named clause - query:

Member [element, cons(element, tail)]
------------------------------------- here {}

Member [element, cons(head, tail)]
---------------------------------- there {
  Member [element, tail]
}

proof {
  Member ["john", cons("paul", cons("john", null))]
  ------------------------------------------------- Member.there {
    Member ["john", cons("john", null)]
    -------------------------------------- Member.here
  }
}

induction datatype + dependent type:

datatype Member (implicit T: Type) (element: T, list: List(T)) {
  here(
    implicit element: T,
    implicit tail: List(T),
  ): Member(element: T, cons(element, tail))

  there(
    implicit element: T,
    implicit head: T,
    implicit tail: List(T),
    prev: Member(element, tail)
  ): Member(element, cons(head, tail))
}

check Member.there(Member.here): Member("john", cons("paul", cons("john", null)))

[xieyuheng]

If inductive datatype have equation above, what about higher inductive datatype?