On Sat, Feb 5, 2022 at 6:10 PM vvs <[email protected]> wrote:
> Hi Mingli,
>
> (2) How can we express something like a type with parameter and the
>> initialization of a type with parameter.
>>
>
> I'm not an expert, so don't take my word for it. But let me guess. Haskell
> is based on simple type theory while set.mm is ZFC, i.e. set theory. They
> are different beasts. You can embed type theory, of course, but that would
> not be set.mm anymore, IMHO.
>
> But maybe some real expert will say that I'm telling nonsensicality and
> this should be easy to do :)
>
That's nonsense, this should be easy to do. :) The equivalent of a type
with a parameter in set.mm is a function from sets to sets. You use
function application to represent the application of the type function to
some particular type.
This has already appeared in this thread: in AV's code you have ( QFrm ` V
) as the type of all quadratic forms over V. Or rather it should read that:
there appears to be an error in the code, and the code as written would
have tripped the definition checker. Here's a revised version (still not
checked though):
${
$d a q v $.
$( The definition of a "quadratic form". (Contributed by ...,
5-Feb-2022.) $)
df-qfrm $a |- QFrm = ( w e. _V |-> { q e. ( ( Base ` ( Scalar ` w ) )
^m ( Base ` w ) ) |
A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )
( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) )
a ) ( .s ` w ) ( q ` v ) ) } ) $.
$}
${
isqfrm.b $e |- B = ( Base ` V ) $.
isqfrm.m $e |- .x. = ( .s ` V ) $.
isqfrm.s $e |- S = ( Scalar ` V ) $.
isqfrm.k $e |- K = ( Base ` S ) $.
isqfrm.t $e |- .X. = ( .r ` S ) $.
$( The predicate "is a quadratic form". (Contributed by ...,
5-Feb-2022.) $)
isqfrm $p |- ( Q e. ( QFrm ` V ) <-> ( Q e. ( K ^m B ) /\ A. v e. B A.
a e. K
( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) )
$=
? $.
$( A quadratic form is a function from a class ` B ` (usually the base
set
of a vector space) to the base set ` K ` of its scalars ` S `
(usually a
field). (Contributed by ..., 5-Feb-2022.) $)
qfrmf $p |- ( Q e. ( QFrm ` V ) -> Q : B --> K ) $=
?$.
$( The property of a quadratic form as a function from a class ` V `
(usually a vector space) to its scalars ` S ` (usually a field).
(Contributed by ..., 5-Feb-2022.) $)
qfrmprop $p |- ( ( Q e. ( QFrm ` V ) /\ X e. B /\ A e. K )
-> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) )
) $=
? $.
$}
Sometimes, when it is important for the input to be a proper class, type
level functions can also be written as term constructors from class to
class instead. For example, the equivalent of Haskell's [a] type, the type
of lists (let's ignore the infinite ones), is "Word A" in set.mm. An
element of Word A is a finite list of elements drawn from A.
There is no particularly convenient way to define inductive datatypes in
metamath as in Haskell, but it is possible to define a type of trees or
other such things via a fixpoint construction. We should probably have a
simpler mechanism for this.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsSQs9%3DtU9-7xA-smNgZdC5Y-VDp4bQ6Bs1koezm%3D-SoA%40mail.gmail.com.
