Open ice1000 opened 5 years ago
I don't want:
GADT syntax (data type)
data X P : I -> Type where
c0 : (x : P) -> X x
c1 : (y : P) -> X y
GACT syntax (dependent records, first-class modules)
codata Y P : I -> Type where
d0 : P
d1 : Blah
Local pattern matching:
case x of
(c0 p0 p1) -> bla
(c1 p0 p1) -> rua
Function level pattern matching:
f : Bla -> Rua
f (c0 p0) = rua
f c1 = bla
Local copattern matching (record constructor syntax):
cocase d0 p0 -> bla
d1 -> rua
Function level copattern matching:
zipWith : [A] -> [B] -> [Coprod A B]
head zipWith (a :: _) (b :: _) = pair a b
tail zipWith (_ :: as) (_ :: bs) = zipWith as bs
Did some try
Type class:
Would the parser be generated by Happy, or be written in vanilla HS? And further, I recommand a document in EBNF-like stuff for users to DIY the parser.
I haven't made an decision yet. Bnf of course will be provided
My proposed data/codata syntax (very early-stage naive version)
-- Coprod: Dependent sum
-- Unit: Unit type
-- <>: Instance search
-- inl/inr: Inject left/right
-- roll: Inductive data type constructor (the "constructor")
-- unroll: Coinductive data type constructor (the "destructor")
F : (A : Type) -> Type
F A = Coprod Unit A
data {F} Nat : Type where
zero : Nat
zero = roll (inl <>)
succ : Nat -> Nat
succ n = roll (inr n)
codata {F} CoNat : Type where
iszero : CoNat -> Type
iszero n = n == zero
pred : CoNat -> CoNat
pred n = unroll (inr n)
n0 : Nat
n0 = zero
n1 : Nat
n1 = succ zero
n2 : Nat
n2 = succ (succ zero)
co0 : CoNat
co0 [| iszero |] = true -- true type
co0 [| pred |] = impossible
co1 : CoNat
co1 [| iszero |] = false -- false type
co1 [| pred |] = co0
Curious: why do we need an "implementation" of the constructors?
data {F} Nat : Type where
zero : Nat
zero = roll (inl <>)
succ : Nat -> Nat
succ n = roll (inr n)
co0 : CoNat
co0 [| iszero |] = true -- true type
co0 [| pred |] = impossible
Disagreed. Should be
co0 : CoNat
co0 [| iszero |] = true -- true type
co0 impossible
Since impossible
is an "inaccessible pattern".
Curious: why do we need an "implementation" of the constructors?
data {F} Nat : Type where zero : Nat zero = roll (inl <>) succ : Nat -> Nat succ n = roll (inr n)
I intended to encapsulate the implementations like Agda's record, emphasizing the fact that the data constructors are based on the endofunctor F
, for instance (mainly from your lagda blog)
record Conat' : Type0 where
inductive
constructor nat
field
succ : Maybe Conat'
open Conat'
toNat' : Conat' -> Nat
toNat' (nat (inl unit)) = O
toNat' (nat (inr x)) = S (toNat' x)
fromNat' : Nat -> Conat'
fromNat' O = nat (inl unit)
fromNat' (S n) = nat (inr (fromNat' n))
I have a point of view that the usual data
from most languages' (generalized) algebraic data types definitions indicate implicit ways to construct data types, e.g.
data Nat : Type where
zero : Nat
succ : Nat -> Nat
This definition explicitly says nothing about how to construct a Nat
, but if we write succ zero
, they will pass the type-check, and here it is the Nat
. Can my goddamn brute talk hold here?
If it holds, we could give the implementations like the Agda's record
to dualize the construction of coinductive types -- we need the endofunctor and a dual inductive natural number zero
.
But to be honest, this design now looks shitty anyway.
This definition explicitly says nothing about how to construct a Nat, but if we write succ zero, they will pass the type-check, and here it is the Nat.
That's right! That's how data constructors work! What else do you expect? Constructors should be like that, in any sense. That's why it's "constructors", not functions. Constructors have different meanings in functional languages, like they can't be reduced. The reason why the can't be reduced is that they have no implementation. Also, terms that contains only constructors and literals are in normal form. This is another example of the difference.
I have some other interesting thoughts coming from Agda, will explain later
This definition explicitly says nothing about how to construct a Nat, but if we write succ zero, they will pass the type-check, and here it is the Nat.
That's right! That's how data constructors work! What else do you expect? Constructors should be like that, in any sense. That's why it's "constructors", not functions. Constructors have different meanings in functional languages, like they can't be reduced. The reason why the can't be reduced is that they have no implementation. Also, terms that contains only constructors and literals are in normal form. This is another example of the difference.
Well... when I was re-arranging my thoughts and materials I read, I realized that I messed up with the concepts of induction and recursion.
We can construct recursive data types by using (impredicative) endofunctor F
, that is, we roll/unroll a type by saying Nat is isomorphic to (Nat + 1) (they have the same structural properties, or we say they have identical roll/unroll mapping between each object).
When it comes to inductive data types, well, bring the hella cute constructors and we all know what is going on!
I will give a further design based on the plain constructors later.
Thanks!
BTW {F}
is an unused variable, how does it work?
data Nat : Type where
zero : Nat
succ : Nat -> Nat
codata CoNat : Type where
iszero : Bool
-- There might be a better way to represent partial function signature
pred : iszero == false -> CoNat
n0 : Nat
n0 = zero
n1 : Nat
n1 = succ zero
n2 : Nat
n2 = succ (succ zero)
co0 : CoNat
co0 [| iszero |] = true -- true type
-- I wanna denote this `pred' pattern is inaccessible, can I?
co0 [| pred |] impossible
co1 : CoNat
co1 [| iszero |] = false -- false type
co1 [| pred |] = co0
Thanks!
BTW
{F}
is an unused variable, how does it work?
It is used by <>
, searching the instance of F
. BTW, you don't sleep you bad bad!
In Agda we have name hints. Say, consider
data OhYesSir : Set where
thankYouSir : (doYouLikeWhatYouSee : Nat) -> OhYesSir
The name doYouLikeWhatYouSee
is not unused. Instead, it's called "name hint" to Agda, and it'll be used during case splits. Consider
meBadBad : OhYesSir -> Unit
meBadBad wryy = {!wryy!}
When we C-c C-c
on the goal, it becomes
meBadBad (ThankYouSir doYouLikeWhatYouSee) = {!!}
without the name doYouLikeWhatYouSee
it'll become
meBadBad (ThankYouSir wryy) = {!!}
This can be used in inductive records -- according to the current design, we can only manually nongchulai inductive records:
data YesYesYesOhMyGod : Set where
recordCons : Nat -> Nat -> YesYesYesOhMyGod
member1 (YesYesYesOhMyGod a _) = a
member2 (YesYesYesOhMyGod _ a) = a
With name hints, we can add some pragmas to auto-gen the projection functions (member1
, member2
), which can be a nice simulation of inductive records.
I want: