These are chat archives for typelevel/scala

12th
Apr 2017
Edmund Noble
@edmundnoble
Apr 12 2017 07:02
Just for the record, the consensus seemed to be that Scato needs a) more testing and b) too much code changed in cats. At the language level, however, it might be more viable. For now, a new library transmogrify (or something related to cats somehow) can supply transformers instead of cats.
Perhaps it will even use the Scato encoding, there may be some specific cases there where it allows user code to be more modular.
Pascal Voitot
@mandubian
Apr 12 2017 07:03
@alexknvl oh I see...
Miles Sabin
@milessabin
Apr 12 2017 07:05
Here is your regular "parametricity is not an unqualified good" PSA: http://stackoverflow.com/a/26012264/146737
Alexander Konovalov
@alexknvl
Apr 12 2017 07:06
If you take the approach that Thorsten Altenkirch and I pioneered (and which my comrades and I began to engineer), the types do form a closed universe, so you don't even need to solve the (frankly worth solving) problem of computing with open datatypes to treat types as data.
Miles Sabin
@milessabin
Apr 12 2017 07:06
(also an observation that we might want to be parametric in non-types)
Edmund Noble
@edmundnoble
Apr 12 2017 07:07
We definitely want to be parametric in non-types, isn't that dependent Scala or at least datakinds?
Alexander Konovalov
@alexknvl
Apr 12 2017 07:08
I am really confused about that answer :confused:
Miles Sabin
@milessabin
Apr 12 2017 07:08

The quote I prefer is the emphasized sentence,

The type of a domain has nothing whatsoever to do with whether quantification over it should be parametric.

Alexander Konovalov
@alexknvl
Apr 12 2017 07:10
I can understand how you can match on types if you have a "closed type 1" for your type parameter.
E.g. ADTs but at the type level.
Edmund Noble
@edmundnoble
Apr 12 2017 07:10
Pining for a proper erasable forall in dependently-typed languages, and acknowledging that using i.e. Generic is essentially removing parametricity.
Because you do know everything about that type. There is no more (parametric) benefit from the abstraction over the type.
Alexander Konovalov
@alexknvl
Apr 12 2017 07:12
a discipline where both parametric/erasable and non-parametric/matchable quantification are distinct and both available
non-parametric quantification = quantification over a closed domain?
Edmund Noble
@edmundnoble
Apr 12 2017 07:13
Matching on a type just means building Generic into the language.
No, it means being able to inspect a value.
Dotted implicits in Idris?
Alexander Konovalov
@alexknvl
Apr 12 2017 07:14
Have not read about them, sorry
How can you inspect a value if your domain is not closed?
Edmund Noble
@edmundnoble
Apr 12 2017 07:14
Essentially a value you can use as an index into indexed type constructors.
The domain of types is closed.
Alexander Konovalov
@alexknvl
Apr 12 2017 07:14
I mean, what are you supposed to compile it to?
Edmund Noble
@edmundnoble
Apr 12 2017 07:14
All of them have a Generic instance.
Miles Sabin
@milessabin
Apr 12 2017 07:15
I don't think it means building Generic into the language, I think it means that Generic is unnecessary in the language because we don't need independent codes to match on. It's of a piece with the "types are really values" DT slogan.
Edmund Noble
@edmundnoble
Apr 12 2017 07:15
Okay so you have passing "dotted" types around which is equivalent to passing around types as now. And you have passing types around which is passing around a representation of the type as well.
I think we're saying the same thing @milessabin.
Miles Sabin
@milessabin
Apr 12 2017 07:15
You can apply the same distinction to non-types.
Edmund Noble
@edmundnoble
Apr 12 2017 07:16
Exactly, and Idris does just that.
Miles Sabin
@milessabin
Apr 12 2017 07:16
Yup.
Edmund Noble
@edmundnoble
Apr 12 2017 07:16
Types and values you can only use to index into type functions, and types and values you can use to index into ordinary functions as well.
@alexknvl You still can't conjure this runtime type information from an arbitrary parametric type variable.
Alexander Konovalov
@alexknvl
Apr 12 2017 07:17
Okay...
So how is it different from passing Generic in?
Miles Sabin
@milessabin
Apr 12 2017 07:18
@edmundnoble non-types can be erased in more contexts than just as indices.
Edmund Noble
@edmundnoble
Apr 12 2017 07:18
Like what?
Miles Sabin
@milessabin
Apr 12 2017 07:19
You can view constant folding or staging as forms of value erasure.
Edmund Noble
@edmundnoble
Apr 12 2017 07:19
@alexknvl It isn't really. It just lets you use that value in the same places as types.
@milessabin I don't follow; in the Idris compiler?
Miles Sabin
@milessabin
Apr 12 2017 07:19
I mean in general.
Alexander Konovalov
@alexknvl
Apr 12 2017 07:20
When you say "non-types", do you mean values?
Edmund Noble
@edmundnoble
Apr 12 2017 07:20
Oh sure. Erasure in general is any injective function.
Parametric values, perhaps?
Miles Sabin
@milessabin
Apr 12 2017 07:21
Types are values, but not all values are types.
... in dependent langs/type theories ...
Alexander Konovalov
@alexknvl
Apr 12 2017 07:23
Okay, I'll get back to this discussion after I read more about DT & TT.
Pascal Voitot
@mandubian
Apr 12 2017 07:28
I'm very fuzzy about type theory and far from catching everything you say
in Idris Type -> Type isn't possible
in a function
you can't pattern match on Types and just practically you see that it should be possible in many cases
Edmund Noble
@edmundnoble
Apr 12 2017 07:30
Cause there's no .Type and Type distinction, all of them are collapsed into .Type.
Even though you could distinguish them, Idris doesn't.
@mandubian Essentially the key is to realize it's a unification of generic representations of types and parameterization on types
Pascal Voitot
@mandubian
Apr 12 2017 07:34
when you say .Type, is it something in idris or something more general in theory?
Pascal Voitot
@mandubian
Apr 12 2017 07:44
@edmundnoble you're refering dot types, right?
.Type is the informational part and Type the physical repr... as .Value=Type and Value=physical repr
Pascal Voitot
@mandubian
Apr 12 2017 07:54
In practice, it's not so trivial to reason about types & values, even in an advanced lang like Idris, because you can manipulate types as values but not exactly...
BTW guys, when you're talking about parametricity, can you define exactly what it is?
parametricy on types only?
Alexander Konovalov
@alexknvl
Apr 12 2017 07:58
open domain universal quantification?
Pascal Voitot
@mandubian
Apr 12 2017 08:00
in other word Forall a?
Alexander Konovalov
@alexknvl
Apr 12 2017 08:01
Well, that's how I used to understand it. But then again, when you do forall a. f a your a is quantified over all types and apparently that's closed domain (because of Generic), so I am not sure what to think anymore :)
Pascal Voitot
@mandubian
Apr 12 2017 08:03
then a dependent type on a value?
is it parametric?
parametricity on non-type things
that was the discussion a bit above :)
Alexander Konovalov
@alexknvl
Apr 12 2017 08:04
I guess that parametric values are those that can be erased, e.g. you take an Int in but you don't "match" on its value
So its value doesn't matter.
Pascal Voitot
@mandubian
Apr 12 2017 08:05
but if you have data A = B | C | D and A -> Type
you could erase it, right?
Alexander Konovalov
@alexknvl
Apr 12 2017 08:06
Not if you match on it
on the value of A
Pascal Voitot
@mandubian
Apr 12 2017 08:06
you mean you can't erase it?
or you can
Alexander Konovalov
@alexknvl
Apr 12 2017 08:07
You can't erase the value of A, unless you don't pattern match.
Pascal Voitot
@mandubian
Apr 12 2017 08:07
yep you can't erase the value of A because you get it from somewhere anyway
but you can erase the uses of f: A -> Type
Alexander Konovalov
@alexknvl
Apr 12 2017 08:08
Again, not if you pattern match on that type somehow...
Consider something like this
f : A -> Type
f A = String
f B = Int
f C = Int
instance Foo String where
  blah = 1
instance Foo Int where
  blah = 2
g : Foo t => (t: Type) -> Int
g _ = blah

main = putStrLn . show . g . f $ A
Pascal Voitot
@mandubian
Apr 12 2017 08:12
yep
when I say "erase" I mean, you could squash A -> Type -> Int to A -> Intafter compiling
the type is erased after applying the functions
Alexander Konovalov
@alexknvl
Apr 12 2017 08:15
What if A is passed at runtime?
Pascal Voitot
@mandubian
Apr 12 2017 08:15
exactly :)
that's what I want to express
Alexander Konovalov
@alexknvl
Apr 12 2017 08:16
Or if your code solves the Collatz conjecture before returning a type.
Pascal Voitot
@mandubian
Apr 12 2017 08:16
in cases, you can erase & in other, you can't
Alexander Konovalov
@alexknvl
Apr 12 2017 08:17
Nvm the latter doesn't matter, it just makes inferring all possible return types harder.
Pascal Voitot
@mandubian
Apr 12 2017 08:17
something I was wondering
Imagine you have a type constructor that are all types datatype F = A | B | C
A, B, C are types
Alexander Konovalov
@alexknvl
Apr 12 2017 08:18
f: A -> IO Type :P
Yeah, that would be what I meant by "closed type 1"
I don't know what the right term is.
Pascal Voitot
@mandubian
Apr 12 2017 08:19
open/closed is fuzzy to me anyway :D
Alexander Konovalov
@alexknvl
Apr 12 2017 08:19
sealed
Pascal Voitot
@mandubian
Apr 12 2017 08:19
ok
but in this case, you can't escape the compile-time
datatype F = A | B | C doesn't really exist outside compile-time
I mean in practice only
not in theory because this is much more complicated ;)
Alexander Konovalov
@alexknvl
Apr 12 2017 08:20
After compilation it would be represented as data F = A | B | C
Pascal Voitot
@mandubian
Apr 12 2017 08:20
but couldn't it just be erased simply?
because in this case, everything is known by the compiler
you get a type A, it becomes a type Int
A disappears
Alexander Konovalov
@alexknvl
Apr 12 2017 08:21
What if I f : Int -> F and then g : (x: Int) -> (f x)?
Pascal Voitot
@mandubian
Apr 12 2017 08:22
but no
datatype F = A | B | C is only a Type :D
no value : F exists
Alexander Konovalov
@alexknvl
Apr 12 2017 08:22
it's not a value
it's type : F
Pascal Voitot
@mandubian
Apr 12 2017 08:23
in current design of types
that's the quesiton of Miles on twitter in some way
to be trivial, I'd like to say type F is (closed) constituted of types A, B, C and A, B, C are Types
just thinking :D
Alexander Konovalov
@alexknvl
Apr 12 2017 08:28
Right. I don't see any problems with it and I think it's a much better design than A -> Type anyway.
Except for the cases where you want to be truly "parametric"
e.g. Option: (a: Type) -> Type
Pascal Voitot
@mandubian
Apr 12 2017 08:30
yep
yet it's interesting because when I write Idris, I see that clearly :D
because I say myself "cool types are values" and then you hit the wall of the limits of this way of thinking :D
because "types aren't exactly values" :D
and then you have to think a bit more
Alexander Konovalov
@alexknvl
Apr 12 2017 08:31
I don't even know how Idris handles cases where you have fmtType: String -> Type, printf: (fmt: String) -> (fmtType fmt)
Seems magic since it's all very unconstrained
interpFormat : Format -> Type
printf : ( s : String ) -> interpFormat ( formatString s )
What if you don't know Format at compilation time,
mmm nvm
Pascal Voitot
@mandubian
Apr 12 2017 08:35
actually you can write the function for all the cases
Format is closed
Alexander Konovalov
@alexknvl
Apr 12 2017 08:35
It's closed but it's defined as an inductive type.
It's closed, I agree
So to call printf on a runtime value you'll have to pattern match on Format and that would allow you to pass the right number of parameters.
So Type there is closed because it depends on Format, which is closed.
Pascal Voitot
@mandubian
Apr 12 2017 08:38
yep
actually how I understand dependent types in practice is "build the whole tree of calls for all possible cases foreseen by your types"
ok my brain has consumed the allowed calories for one day... now time to work :D
Miles Sabin
@milessabin
Apr 12 2017 09:38
"build the whole tree of calls for all possible cases foreseen by your types"
:+1:
jeremyrsmith
@jeremyrsmith
Apr 12 2017 17:40
speaking of dependent types, what’s a use case for instance-dependent types? I can’t think of one
I.e. if I have trait Foo[T] { type Out }, I can’t think of why I would want two different Foo[Int] instances to have a different Out
Edmund Noble
@edmundnoble
Apr 12 2017 18:00
For the same reason you'd want two different types A and A2 in your Foo[Int, A] and Foo[Int, A2] instances. Except without affecting type inference.
For instance: you could distinguish between two Ordering instances' types using a phantom type member, to avoid mixing Ordering instances by accident.
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:27
@edmundnoble I think in that case you would use a type arg, not a type member. If your goal is to differentiate two different instances, then you want all the different things about them to be involved in the implicit search. Otherwise you don’t know which one you’re. getting (and you’ll probably get divergence to boot)
Edmund Noble
@edmundnoble
Apr 12 2017 18:28
Yeah TBH I haven't seen any cases in the wild of keeping the same T and varying the type member, because that no longer adheres to the "implicit search to implement type functions" idea.
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:29
that’s my problem; I can’t think of any use cases (that I agree with) for dependent types where they’re not in some sense a type function
Edmund Noble
@edmundnoble
Apr 12 2017 18:29
Well in that case you must have a divergence issue.
Greg Pfeil
@sellout
Apr 12 2017 18:29
I’ve been considering one case (well, a pair of them) in Matryoshka that varies the type member …
Edmund Noble
@edmundnoble
Apr 12 2017 18:30
Oh yes? RecursiveT?
Greg Pfeil
@sellout
Apr 12 2017 18:30
Well, Recursive[Cofree[F, A]] and Corecursive[Free[F, A]].
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:30
and many things would be so much easier if we just said “dependent types of a typeclass are a type function and the dependent type(s) must be stable in the type argument(s)"
Edmund Noble
@edmundnoble
Apr 12 2017 18:31
@jeremyrsmith Oh certainly. But I think that makes other subtyping-based usages of type members illegal.
@sellout we're talking varying the type member while keeping the type parameters the same.
Greg Pfeil
@sellout
Apr 12 2017 18:31
There is a Birecursive.Aux[Cofree[F, A], EnvT[A, F, ?]], but there’s also potentially a Recursive.Aux[Cofree[F, A], F] that just ignores the annotation.
And the dual of that for Free
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:32
You could say it only for the purposes of implicit-based type inference
Edmund Noble
@edmundnoble
Apr 12 2017 18:32
@jeremyrsmith The Aux pattern, though.
(also implicit-based type inference is bidirectional at the moment, which I think stops if you change that)
Essentially why @sellout's variant is safe (in terms of divergence) is that the type member must be referred to in method calls that try to access the typeclass.
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:33
I.e. if I do an implicit search for Foo[T] which has type member Out, then I may resolve a different instance in different places, but Out will always be the same and I can cache it (and use it to refine the same search for Foo[T] subsequently)
Edmund Noble
@edmundnoble
Apr 12 2017 18:34
So some form of coherence?
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:35
I know it’ll never happen… I just can’t think of a use case where you explicitly would want the type member to vary in implicit search
at least a sane one
Edmund Noble
@edmundnoble
Apr 12 2017 18:36
@sellout seems to have a good reason: implicits that are based on other implicits only use the type member abstractly, and user code using implicits uses the Aux pattern.
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:38
well, in that case I feel that it’s conceptually a type argument and you only want it to be a type member in order to reference it at type level
in that case you could make it a type argument and a fixed type member that captures the type arg
Olivier Toupin
@oliviertoupin
Apr 12 2017 18:40
Hi, I'm wondering if there is a backport for 2.11 for this PR
scala/scala#5649
We are stuck on 2.11 because of Spark
Greg Pfeil
@sellout
Apr 12 2017 18:41
@jeremyrsmith Well, I feel like it’s a type member, and those instances are cheating a bit for convenience … and the Aux part should be avoidable with interlaced implicits …
jeremyrsmith
@jeremyrsmith
Apr 12 2017 18:41
what would be great is a way to explicitly mark a type member as stable over some type arguments
I started on a compiler plugin to do that but my tiny brain didn’t have room for the bulk of the scala compiler that was involved
@sellout I probably misunderstand what you were saying… my tiny brain can’t seem to contain matryoshka either :)
Greg Pfeil
@sellout
Apr 12 2017 18:46
@oliviertoupin We have that issue, too. Our “solution” is to break it into smaller repos, so in development we can take advantage of 2.12 for most of it, then only in Travis and in the Spark-dependent part do we have to use 2.11.
@oliviertoupin But that modularization was something we planned independently. It just also solves that problem for most of our code.
Greg Pfeil
@sellout
Apr 12 2017 18:54
@jeremyrsmith Well, the idea of (Bir|Cor|R)ecursive is that it takes some type and associates it with the an equivalent type with the recursion removed. So, for List[A], that’s ListF[A, ?], for Cofree[F, A], it’s EnvT[A, F, ?] (which is the transformer for (A, F[?])). But in the case of Cofree we can cheat a bit by just throwing away the (A, _), giving us a second instance. This is useful for us because sometimes we’d like to use a constraint like Recursive.Aux[T, F], but that means that we can’t use Cofree there. So far we’ve been able to get around it by rather than using the implicit constraint, we ask for an explicit A => F[A], which is usually just Recursive.project, but for Cofree is Recursive.project >>> EnvT.lower.
andy scott
@andyscott
Apr 12 2017 19:22
@mandubian for kind poly in TLS, is there a known issue about using the feature across SBT modules/compliation boundaries? I’ve defined some KP types that work correctly if I use them in the same module, but as soon as I try to leverage the KP from my tests, the compiler yells.
Pascal Voitot
@mandubian
Apr 12 2017 19:34
@andyscott Interesting
andy scott
@andyscott
Apr 12 2017 19:34
yeah :frowning:
Pascal Voitot
@mandubian
Apr 12 2017 19:34
I must say I haven't tried in multiple module
Greg Pfeil
@sellout
Apr 12 2017 19:34
This could put a wrench in my Polydactyl plans 😆
Pascal Voitot
@mandubian
Apr 12 2017 19:35
hehe :)
andy scott
@andyscott
Apr 12 2017 19:35
Eeh
If there’s a bug, we can fix it, right? :smile:
Pascal Voitot
@mandubian
Apr 12 2017 19:35
that msut something stupid
andy scott
@andyscott
Apr 12 2017 19:35
And then get a new TLS hotfix or snapshot release to toy with
I wonder if it’s an issue with the erasure phase obscuring the AnyKind across the module boundary?
Pascal Voitot
@mandubian
Apr 12 2017 19:36
@andyscott can you make a mini sample project to reprocue it?
andy scott
@andyscott
Apr 12 2017 19:36
Yes
Greg Pfeil
@sellout
Apr 12 2017 19:36
Yeah – I’m sure @milessabin is looking for an opportunity to push CrossVersions.patch adoption :)
Pascal Voitot
@mandubian
Apr 12 2017 19:36
@andyscott good remark on erasure
you're right!
andy scott
@andyscott
Apr 12 2017 19:36
Well, I was looking at your implementation and that’s what came to mind
I can has fix it, I think
Pascal Voitot
@mandubian
Apr 12 2017 19:40
it's funny because I was focused on erasing everything
but maybe it's bad to erase so much :D
andy scott
@andyscott
Apr 12 2017 19:40
You did a great job of that
:grin:
Pascal Voitot
@mandubian
Apr 12 2017 19:41
but that's a good idea to test things in external compile unit
I should have done that
andy scott
@andyscott
Apr 12 2017 19:41
I’ll put together a test for you
Pascal Voitot
@mandubian
Apr 12 2017 19:41
great!
andy scott
@andyscott
Apr 12 2017 19:41
against scalac, and try a fix quickly
Pascal Voitot
@mandubian
Apr 12 2017 19:42
even greater
anyway, i'm sure there are still issues
this is a first version
we need to push KP further
Pascal Voitot
@mandubian
Apr 12 2017 19:50
The other day I was wondering whether it would be possible to have a new field in Type that contain the Kind of the Type
andy scott
@andyscott
Apr 12 2017 19:51
Oh man, I forgot how gloriosly long it takes to compile scalac and std lib
Pascal Voitot
@mandubian
Apr 12 2017 19:53
first time ;)
andy scott
@andyscott
Apr 12 2017 19:53
First time compiling your branch, at least
andy scott
@andyscott
Apr 12 2017 20:10
It works across runs in partest, but fails in my SBT project.
Same exact code too.
KPs are enabled for my test configuration too— KP code in the test directory works on its own right.
Alexander Konovalov
@alexknvl
Apr 12 2017 21:39
@jeremyrsmith There are some legit cases where you forget your type member completely, so it can't be used for implicit resolution.
There are cases where coherence breaks down, so different Foo[T] instances have different type members.
You just need to add some side-effects :fire:
Or just local implicits.
Actually in the latter two cases you need to actually forget your type member anyway.