~thon/thon

ref: 5180b858109c12b20eac00c11eff87b0f5dc993a thon/syntax.org -rw-r--r-- 11.6 KiB
5180b858Evan Bergeron Use List in datatype example 4 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
|------------+-------------------+----------------------------------------------------------------------------------------------------------------------------------------------+--------------+--------------+--------------------------------------------------+------------------+---------+---------------+--------------+---|
| sml        | fun foo a =       | signature Thong = sig .. end and structure Thon :> THON struct end OR structure Thon : sig type type someSig val end = struct someStruct end | a : int      | if then else | datatype a Some =                                | module shit      | let a = | async stuff   | records      |   |
|------------+-------------------+----------------------------------------------------------------------------------------------------------------------------------------------+--------------+--------------+--------------------------------------------------+------------------+---------+---------------+--------------+---|
| haskell    | foo a = or \ a -> | class Thon a where someStruct AND instance Thon bool where                                                                                   | a :: Integer | if then else | data Maybe a = None \  Some a or type (no ctors) | class Eq a where | a =     |               |              |   |
| ocaml      | let               |                                                                                                                                              |              |              |                                                  |                  |         |               |              |   |
| coq        | fun foo =>        |                                                                                                                                              |              |              |                                                  |                  |         |               |              |   |
| elm        |                   |                                                                                                                                              |              |              |                                                  |                  |         |               |              |   |
| purescript | let or \          |                                                                                                                                              |              |              |                                                  |                  |         |               |              |   |
| alice      |                   |                                                                                                                                              |              |              |                                                  |                  |         | spawn or lazy |              |   |
| idris      | foo a =           |                                                                                                                                              |              |              | similar to haskell                               |                  |         |               | record where |   |
| f#         | let foo a =       |                                                                                                                                              |              |              | type Maybe = None                                | Some of          |         |               | async        |   |
| rust       |                   | trait ThonTrait {} AND impl ThonTrait for SomeStruct {}                                                                                      |              |              |                                                  |                  |         |               |              |   |
|------------+-------------------+----------------------------------------------------------------------------------------------------------------------------------------------+--------------+--------------+--------------------------------------------------+------------------+---------+---------------+--------------+---|

or just like yah traits are types so with type var names could just say


* Typeclasses / modules should feel like functions.
** Introduction / definition
The argument is the module structure, of type signature.
This relationship is many-to-many.

"Moreover, a given module may well support a variety of views, for
example by “forgetting” certain aspects of it in particular contexts.
For example, one may neglect that an implementation of mapping
supports deletion in a setting where only extension and application
are required."

This is likely why subclassing is ideal...

** Bob has two criticisms of typeclasses
*** They insist that a type can implement a type class in exactly one way. 
    This is true of rust traits as well.
*** They confound two separate issues: specifying how a type implements a type class and specifying when such a specification should be used during type inference.  
(See the borked example above).

sign Foo = ()

* The syntax
*** type someNatList = some t (t, (nat, t) -> t)
    matches lambda syntax and that works same as subst.
*** trait someNatList t = (t, (nat, t) -> t)
*** impl (someNatList t) as pkgImpl
*** impl (some t  (t, (nat, t) -> t)) as pkgImpl
*** use pkg as l : someNatList t in
puts impl, and type var at the front
** Defining a signature is different than defining a package. Signatures are types; packages are expressions.
** Defining a signature is defining a type.
some types are parametrized. usually this means universal parametrization.
but here we have existential...
*** [sugar-free] type someNatList = some t (t, (nat, t) -> t)
    matches lambda syntax and that works same as subst.
*** [GOOD] trait someNatList t = (t, (nat, t) -> t)
    not sure about the =
and just restrict it to one or the other entirely. can't mix ALL and SOME.
*** type someNatList (some t) = (t, (nat, t) -> t)
*** sig someNatList t = (t, (nat, t) -> t)
*** sig someNatList t where (t, (nat, t) -> t)
*** sign someNatList t is (t, (nat, t) -> t)
*** interface someNatList t = (t, (nat, t) -> t)
** Usage: traits are parametrized types; they go everywhere types go.
Just need a way to define the internal type also (without creating a var name).
Or maybe we just allow both or none?
*** [PFPL] open pkg as l : some t (t, (nat, t) -> t)
binds a fresh type variable t.
*** use pkg as l : someNatList t in
*** l : some t (t, (nat, t) -> t) = pkg
the same as 
open l
*** l : someNatList t = pkg
*** l : someNatList t



struct Foo a (
) : ()

maybe another way to put it is just that some types define interfaces.
and there is a subtyping relation between these (eventually....)

** Defining a package is defining an expression.
*** Thoughts
But you have to provide a type also. So it's like a lambda. It's just
a chunk of reusable code. \ (foo : nat) -> ye
type t. nice to have a keyword or char at the front to identify.

\ (x : nat) -> foo

it's like a \ also bc it's a value. it's not being "called". but the
binding structure is different. there's no "argument name"; the
argument is the impl type.

\ implType -> pkgImpl

It's like a polymorphic function. You're instantiating the
polymorphism, but leaving the function part. Providing a type.

*** [PFPL] pack implType with pkgImpl as (t, (nat, t) -> t)
*** [GOOD] impl (someNatList t) as pkgImpl (puts impl and trait name at the front - pretty readable. puts details in the back)
*** [GOOD] impl (some t . t, (nat, t) -> t) as pkgImpl (puts impl and trait name at the front - pretty readable. puts details in the back)
*** pkgImpl deriving (some t (t, (nat, t) -> t)) [similar to rust, haskell?]
*** impl (some t (t, (nat, t) -> t)) as pkgImpl
similar to deriving clause of haskell typeclasses, but is at expression layer not type layer.
similar to impl () for () { } in rust, but it's a many-to-many relationship between impls and sigs
but i think in rust, for a fixed "struct type" and fixed trait, there is a single impl.
not the case here. fix a tuple type and a sign. impl() 

*** pkgImpl deriving (someNatList t) [similar to rust, haskell?]
similar to haskell, but it's at the expression layer, not the type definition layer. so bit more flexible?

*** pkg : some t (t, (nat, t) -> t) = pkgImpl
*** pkg : (someNatList t) = pkgImpl [good, but forces a name decl]
*** pkgImpl : (someNatList t) [good, but forces a name decl]
*** pkgImpl (someNatList t) [good, but forces a name decl]
*** pack implType with pkgImpl as someNatList
*** impl someNatList t = pkgImpl
*** struct pkg : someNatList implType = pkgImpl
*** pkgImpl : someNatList implType


* Elimination / calling

defining the signature should feel like a defining a function
defining the structure should feel like calling a function

https://existentialtype.wordpress.com/2011/04/16/modules-matter-most/


class Foo natlist trait

type someNatList = some t (t, (nat, t) -> t)
sugar to
class someNatList t where (t, (nat, t) -> t)
or
class someNatList t = (t, (nat, t) -> t)

instance 

then we just define an object of this type.
name : t = ...
NatList : someNatList = ( , )

could spell it out as
NatList : some t (t, (nat, t) -> t) = ( , )



the thing i want to avoid (i think) is having a separate object for "traits" and "types"....

that's a nice thing about the pack model: there's not really a separate notion of traits, a trait is a type.

haha
FOLD IS CAST
TRAITS ARE TYPES

one nice thing about rust is it can impl many traits on a single struct.
maybe sml and haskell can do the same?

can also do
signature THON = sig ... end

struct Thon :> THON =
struct
end

so tldr is basic stuff should look like haskell or idris.
english language keywords over symbols
\ as lambda
: for typing
case of
no let or var or val or fun
probs skip `of` for datatype definitions
also list comphrensions cause list comphrensions are great.

here's the overlapping typeclass issue from haskell

-- file: ch06/Overlap.hs



instance Borked Int where
    bork = show

instance Borked (Int, Int) where
    bork (a, b) = bork a ++ ", " ++ bork b

instance (Borked a, Borked b) => Borked (a, b) where
    bork (a, b) = ">>" ++ bork a ++ " " ++ bork b ++ "<<"
    
We have two instances of the typeclass Borked for pairs: one for a pair of Ints and another for a pair of anything else that's Borked. No comments

Suppose that we want to bork a pair of Int values. To do so, the compiler must choose an instance to use. Because these instances are right next to each other, it may seem that it could simply choose the more specific instance. 2 comments

However, GHC is conservative by default, and insists that there must be only one possible instance that it can use. It will thus report an error if we try to use bork.


some nice more sugar:

data DataInt = D Int
    deriving (Eq, Ord, Show)
* possible words
port trait lot pack
could use symbols too;

* Down the line
data natlist = nil | nat * natlist;
trait Stack t = (t * ((nat * t) -> t))

impl Queue natlist as (...)
impl Queue (natlist, natlist) as (...)

eventually, want something like
```(u. (unit |  (nat * 0)))```
becomes
```data natlist = nil | nat * natlist;```
and
```0 * ((nat * 0) -> 0)```
becomes
```some t (t * ((nat * t) -> t))```
or 
```trait Stack = (t * ((nat * t) -> t))```
and then
```impl (0 * ((nat * 0) -> 0)) with (u. (unit |  (nat * 0))) as```
becomes
```impl (some t (t * ((nat * t) -> t))) with (natlist) as```
or
```impl (Stack) with (natlist) as```
or
```impl Stack natlist as```

so the whole program could look like
```
data natlist = nil | nat * natlist;
trait Stack t = (t * ((nat * t) -> t))
impl Stack natlist as (...)
```

* requires and ensures clause
taken from fortress
factorial(n) requires (n>=0) ensures (result >= 0) =
* s = [ x | x > 0] would be nice