Replies: 3 comments 12 replies
-
|
It seems like you understand
Line 365 in 39b4bec S there are no concrete things in Koka of kind h. It must be a type-variable, or global.
// Use `run` to dismiss the state effect
pub fun work-on-my-heap() : <console> ()
with run
work-on-any-heap()
pub fun main()
work-on-string-value("Hello")
work-on-int-value(2)
// work-on-global-heap()
work-on-my-heap() // No state effect observable
() |
Beta Was this translation helpful? Give feedback.
-
Yaay!! 😃
Oh, good to know, so I can forget about them.
Okay, I see. So the actual kind is Could you give me an example what Regarding understanding abstract type precious<a> :: V -> V
Precious // private, because of abstract type!
pub fun keep-precious( x : precious<a> ) : console ()
println("Hello.")
()
pub fun pass-precious( x : precious<a> ) : console ()
println("---")
keep-precious(x)
println("World.")
println("---")
()
pub fun leak-precious( x : precious<a> ) : console precious<a>
println("Leaking.")
x
pub fun run-with-precious( action : forall<a> precious<a> -> e t ) : e t
action(Precious)
pub fun main()
run-with-precious(keep-precious)
run-with-precious(pass-precious)
//run-with-precious(leak-precious) // won't work
()Now looking at the types of
Now So when I comment-in the last line, I get: I think I understood this now, but feel free to correct me if I'm wrong. 😅
If I understand right, then I used So the type argument is just polymorphic.
Doesn't declaring Would it be (theoretically) possible to replace the kinds Thank you for all your explanations. 🙏 I hope I got a bit closer to understanding kinds in Koka (and how higher-rank polymorphism and the |
Beta Was this translation helpful? Give feedback.
-
|
To understand the kind of handlers read this, and the next few paragraphs: Line 50 in 39b4bec Yes, you could technically use The advantage of keeping them separate is mostly for documentation -> for example you have no field in Additionally, |
Beta Was this translation helpful? Give feedback.
-
|
From all that info, I would like to try to give a short overview of how I understand kinds now in general and also with respect to Koka (including the syntax). I hope I got it right, and I'm also happy to be corrected where I'm wrong. There are values, types, and kinds. Each value is of a specific type and each type is of a specific kind. To denote a variable Most usual types we deal with in programming are of kind A function type (which is a value type and thus of kind Types are inhabited if there is at least one possible value of the type. Types that are inhabited are always of kind If a type has only one possible value, it is inhabited but practically carries no information. Koka comes with a So let's sum up some examples for value types, i.e. types of kind
As both the type of arguments and the type of a return value may be a function (functions are first-class values in Koka), we can also have more complex value types like:
Moreover, it's possible that functions are polymorphic, which means they accept values of arbitrary types as arguments and their return type may depend on those input types. When we use single lowercase letters, then Koka automatically treats these as type variables rather than specific types. For example To explicitly denote an identifier as a variable, we can use the The syntax when defining a function is slightly different. Both functions below have the same type: fun my-func<foo>( x : foo ) : foo
x
fun same-func( x : a ) : a
xWhen defining a function, the colon ( As we can have functions which expect or return polymorphic functions, it is also possible to use such polymorphic types as an argument or return type of a function. For example: fun some-func( pick : forall<a> (a, a, bool) -> a ) : console ()
println( pick(3, 7, True ).show() )
println( pick("Hello", "World", False ) )
pub fun main()
some-func( fn(x, y, b) if b then x else y )Here, the So some more examples of value types (recall that all these are still of kind
Now all this is pretty complex already, but only covered types of kind Now how many other kinds are existing? There are the built-in types For example And example would be the following type: type one-or-two<a> :: V -> V
One ( only : a )
Two ( first : a, second : a )It is optional to annotate the kind with We can also take two value types as arguments for such a type constructor: type different<a,b> :: (V,V) -> V
First ( only : a )
Second ( only : b )
Both ( first : a, second : b )But we can also accept type constructors (e.g. a type of kind type nested<c,a> :: (V->V, V) -> V
Easy ( easy : a )
Complex ( complex : c<a> )So just using the basic kind Now to the kinds These types aren't usually named so they don't need and cannot be referenced in code, with the exception that When a function's type signature includes types of kinds Effect rows (sets of effects, but each effect may appear more than once) are types of kind pub fun twice<effty::E,valty::V>(func : () -> effty valty) : effty (valty,valty)
(func(), func())Or in short, using single letter variables: pub fun twice(func : () -> e v) : e (v,v)
(func(), func())Until here, I covered the kinds However, I'm still confused about |
Beta Was this translation helpful? Give feedback.
-
|
You wrote earlier:
But something still doesn't fit. Consider: fun my-func<foo>( x : foo ) : foo
x
val my-func-clone : (forall<a> a -> a) = my-func
alias compiles :: V = (forall<a> a -> a)
val my-func-clone2 : compiles = my-func
//alias does-not-compile :: V -> V = (forall<a> a -> a)If I uncomment the last line, I get: This leads me to the impression that in This also seems to make sense: Note that What do you think? |
Beta Was this translation helpful? Give feedback.
-
|
That makes sense, sorry for leading you down a wrong path. I should have checked. I still find it interesting that the kind of the type that it has isn't reflective of the type parameter. It means that this introduction form in the language doesn't match the behavior of other introduction forms (constructors). Particularly, I would expect that even though |
Beta Was this translation helpful? Give feedback.
-
No problem, it is interesting as it's easy to confuse kinds and types here (also due to the syntax, where both
Not the kind system, but the type system, I believe. Function arguments must be values (when calling) or value types (when defining). Thus the type Another example: fun swap<h::H,a::V>( cell1 : ref<h,a>, cell2 : ref<h,a> ) : <div,st<h>> ()
val tmp = !cell1
cell1 := !cell2
cell2 := tmp
alias type-of-swap :: V = forall<h::H,a::V> (ref<h,a>,ref<h,a>) -> <div,st<h>> ()
val swap2 : type-of-swap = swapLet me try to summarize the example above:
However, it's not possible to store polymorphic functions such as So getting back to the original example:
|
Beta Was this translation helpful? Give feedback.
-
|
Yeah that makes sense. I understand how it is currently treated. I'm just wondering out loud whether it needs to be treated like that, or if function types can be treated more like datatypes. In other words, does the theory where I think it is more of a technical limitation than theoretical. For example, function types can be inferred and generalized which means that the number and kinds of type parameters that need kind inference is not available until after type inference. Whereas polymorphic datatypes always need annotation in Koka currently. So it seems we do a sort of partial kind inference - for types and for explicitly annotated type variables, and don't even attempt to give functions more complex kinds, although they theoretically could have them? |
Beta Was this translation helpful? Give feedback.
-
I think a potential problem could be what I wrote here:
So in other words, if the type
But perhaps there is another problem. Let's assume the type of val my-passes0 : list<poly-pass> = Cons(my-id, Nil)we would attempt to pass a type of kind Some more Koka fun: fun my-id<a>(x : a) : a { x }
alias poly-pass<a> :: V -> V = a -> a
alias crunch<t :: V -> V> :: (V -> V) -> V = forall<a> t<a> // doesn't work as wanted
val my-int-id : poly-pass<int> = my-id
val my-string-id : poly-pass<string> = my-id
//val my-poly-id0 : poly-pass = my-id // doesn't work
//val my-poly-id1 : crunch<poly-pass> = my-id // surprisingly doesn't work either
val my-poly-id2 : forall<a> poly-pass<a> = my-id // but this works
//val my-passes0 : list<poly-pass> = Cons(my-id, Nil) // doesn't work
//val my-passes1 : list<crunch<poly-pass>> = Cons(my-id, Nil) // doesn't work
val my-passes2 : list<forall<a> poly-pass<a>> = Cons(my-id, Nil) // this worksAttempting to uncomment the So apparently Koka doesn't recognize that |
Beta Was this translation helpful? Give feedback.
-
|
In my previous post, I gave this example: pub fun twice<effty::E,valty::V>(func : () -> effty valty) : effty valty
func()
func()Now trying to modify it to: pub fun twice<atm::X,valty::V>(func : () -> <atm> valty) : <atm> (valty,valty)
(func(), func())Gives the following compile error: I learned earlier that
So does that mean -pub fun twice<atm::X,valty::V>(func : () -> <atm> valty) : <atm> (valty,valty)
+pub fun twice<atm::HX,valty::V>(func : () -> <atm> valty) : <atm> (valty,valty)
(func(), func())Now I get: Let's see if HX can be used at all. Apparently the following compiles: effect my-effect1 :: HX
fun log1 ( msg : string ) : ()
effect my-effect2 :: (E,V) -> V
fun log2 ( msg : string ) : ()Okay, so if I declare an effect, that effect has kind I tried to read the notes in
Side note: I assume that the kind of That "answer context" is explained as:
Okay, so when we have some type (say That makes sense to me now, but… what I wonder is whether this is just some language internals? Or does it ever make sense to actually use values of these type in Koka "user" code? E.g. would I ever use the I would like to understand how much of this is actually internals, and which of it is intended to be used by user code? Also, how does Sorry for my confusion. |
Beta Was this translation helpful? Give feedback.
-
|
I believe that The note is indeed a little imprecise. I believe the type parameters are given You are trying to tie this down to implementation details a bit too much. Types and kinds are used by the compiler for ensuring valid programs, but then are erased completely when compiling. Even in As far as I understand it the relationship between X and HX is if the effect is known to be handled it is of kind |
Beta Was this translation helpful? Give feedback.
-
|
Thanks for your explanations! 👍 |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
-
I would like to better understand kinds and how they are used.
The book lists some kinds, which I will try to enrich with examples:
V: value type, e.g.intorstringX: (atomic) effect type, e.g.exnordivE: effect row, e.g.total,pure, or<ndet,console>H: heap type, e.g.global(and any other!?)S: scope type (which is only created implicitly by ax <- named handlerexpression?)P: predicate type (not sure what that is and if it's used somewhere?)HX: "handled effect type" (which means?), likely defined as some sort of kind-alias(?) for(E,V) -> VHX1: "handled linear effect type"If I write:
Then I get:
But I think
goodyshould beHX1andmoodyshould beHX? Why do both show the same kind?Now this makes me also wonder about the
->notation. As far as I understand, for types it denotes functions:string -> intis the type of a function that gets astringand returns anint.Also, such a function again has the kind
V, it seems:But even functions involving effects seem to be of kind
V:I guess that's because those are first-class values (hence
V), like any other value of a primitive datatype such asint?When using the
->operator for kinds, it means it's some sort of higher-ranked "function"(?), like a type constructor, right? E.g.(V,V) -> Vis a type constructor that takes two (arbitrary?) types of kindVand returns a type of kindV. For example:I feed in a pair of (value-)types and get another (value-)type back. As far as I understand, there is no restriction on the value types I feed into
oneortwo: the only restriction is that it's value types, i.e.intorstring -> intor() -> exn intand not, for exampleexn, which would be of kindX(orEdepending on context?).But then, I don't understand the notion of
(E, V) -> V. Does it meanmoodyfrom above can take any (arbitrary?) row of effects and any (arbitrary?) value-type (such as a function type) and return another value-type (such as a modified function type)? Or how does it work? And what role does the row of effects play there? Could someone point me to a particular example which types of kindEandVcould be fed in, and which type of kindVcould be returned?Another issue I don't understand is what the
Hkind really is.Consider I have a function:
This has type:
Thus I assume I can use this function with any heap
h, right? And I can use it for different heaps in the same program? But how do I create such a heap? Is it as easy as writing:? Or do I have to use a specific function or keyword for it? If yes, which one(s)?
I tried some things, and it confused me more than giving answers:
Running this as is, I get
5as a result. But if I uncomment the last line:Then I get:
Why does the compiler expect these effect rows to be identical? It also doesn't expect the
work-on-string-valueandwork-on-int-valuefunctions to be identical.If I only comment in the last line:
Then I get:
Is there any way to use other heaps than
global? How does this really work and is there some documentation on it, or example code?I'm sorry if I maybe misunderstand quite a lot as of yet. I'd appreciate any help to get a better overview on the topic of "kinds" in Koka.
Beta Was this translation helpful? Give feedback.
All reactions