Re: [isabelle] a line of type definition



This is a way of representing an N-dimensional vector space as a type, even though higher-order logic does not have dependent types. The idea is to represent the number N by a type having that many elements.

John Harrison invented this idea, and his exposition is still the best:

http://link.springer.com/article/10.1007%2Fs10817-012-9250-9

Larry Paulson


On 15 May 2014, at 10:43, yongjian Li <lyj238 at ios.ac.cn> wrote:

> Dear experts:
>  I read line 2404 in Determinats.thy, which is listed as follows:
> 
> definition trace :: "'a::semiring_1^'n^'n &#8658; 'a"
>  where "trace A = setsum (λi. ((A$i)$i)) (UNIV::'n set)"
> 
> I can guess A is of type 'a matrix, returns a result with type 'a.    (informally)
> 
> This is the first time I meet the type cat operator ^, can some experts
> interpret it?       
> 
> Or simply point me which tutorial material I should read .
> 
> regards!
> 		





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.