mro has quit [Read error: Connection reset by peer]
mro has joined #ocaml
mro has quit [Read error: Connection reset by peer]
<ski>
olle : that's the link that was shown before i think (?). yea, reasonably so
mro has joined #ocaml
<olle>
Alright, well just ask if something is not :)
bartholin has joined #ocaml
perrierjouet has joined #ocaml
<ski>
olle : well, i don't see what that post has to do with concatenative languages or stacks
mro has quit [Quit: Leaving...]
Stumpfenstiel has joined #ocaml
bartholin has quit [Ping timeout: 260 seconds]
<olle>
ski: The stack can be simulated inside the type-system, so you move errors from runtime to compile-time
wonko has quit [Ping timeout: 268 seconds]
<ski>
yes
<ski>
i figured out one way to do it, years ago. might be the same as the one mentioned in Armael's link (haven't checked yet). you can also do it with pairs
<ski>
but i'm not sure how (or in which sense) phantom types would fit in
<olle>
Since a word in forth expects a certain stack structure, the function would accept a stack state with the correct type only
fuji has left #ocaml [#ocaml]
<ski>
oh, you mean like a "vector" GADT / indexed family, indexed by peano yes
<ski>
(sorry, when i hear "phantom", i don't directly think of GADT)
<olle>
Not sure what that is
<olle>
No, GADT is not phantom, true
<olle>
You'd have to check examples further down in the thread, unrelated to GADT
rgrinberg has joined #ocaml
<ski>
"that" being ?
<ski>
oh, vector
<ski>
in Haskell terms, `data Vector a :: Nat -> Type where Nil :: Vector Zero; Cons :: a -> Vector a n -> Vector a (Succ n)'. here `data Nat = Zero | Succ Nat' is a (`data' type promoted to a) `data' kind
<ski>
(in Agda it's basically the same, except there's no need to "promote", type of `Vector' can be `Set0 -> Nat -> Set0' with `Set0' being a `Set1' and `Nat' being a `Set0')
<olle>
Hm
<ski>
(.. but in your case, you'd want to index by a list of types, rather than a peano natural, i guess. `data Stack :: [Type] -> Type; Nil :: Stack '[]; Cons :: a -> Stack as -> Stack (a ': as)')
<ski>
(in OCaml, i think without promotion, you could use `type Zero',`type 'a Succ', or `type Nil',`type ('a,'as) Cons' ?)
<olle>
Not much resources out there, mostly related to embedded boards
<olle>
Gotta sleep, see ya \o
<ski>
g'night
* ski
should try out some Commodore 64 Forths
<ski>
e.g. ultraForth^WvolksForth, since CC64 (a (non-cross) C compiler on the C64) was written using that, by Philip Zembrod. he's recently taking up coding on it, again
olle has quit [Ping timeout: 260 seconds]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
wingsorc has quit [Remote host closed the connection]
wingsorc has joined #ocaml
wingsorc has quit [Remote host closed the connection]
Haudegen has quit [Ping timeout: 248 seconds]
wingsorc has joined #ocaml
Stumpfenstiel has quit [Ping timeout: 246 seconds]
wingsorc has quit [Remote host closed the connection]
azimut has quit [Ping timeout: 258 seconds]
wingsorc has joined #ocaml
wonko has quit [Ping timeout: 260 seconds]
wingsorc has quit [Remote host closed the connection]