For the type level gurus: I would like to define types Sum :: [Field] -> * (:::) :: String -> * -> Field used like this Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ] (I hope this makes sense. I'm not quite familiar with the syntax.) such that Sum '[ s1 ::: a1, ... ] unifies with Sum '[ s1 ::: b1, ... ] to give Sum '[ s1 ::: c1, ... ] where c1 is the unification of a1 and b1. If sn is absent from exactly one of the unificands then its type is copied over unchanged. If sn is absent from both then it is absent from the unification. The types should also be invariant under permutation of the list. This is perhaps a bit obscure so I'll explain the application. This is intended for the sumtype equivalent of a record type, so if we have Sum '[ "foo" ::: a, "bar" ::: b ] and Sum '[ "foo" ::: a, "baz" ::: c ] then I take take the sum of these sums and get something of type Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ] If it makes it easier than I am happy for Sum '[ s1 ::: a1, ... ] to unify with forall ak. Sum '[ s1 ::: a1, ..., sk ::: ak ] This is justified by forall b. Either a b being isomorphic to a. Is such a type possible? If so my next question will be about how to type deconstructors of such things, but let's start with a small first step! Thanks, Tom
I'm not going to do the whole thing for you but I can help start you off. The type level string you think of is called Symbol. Symbol is a kind on it's own and not (*) it has a type for every string. You can use the functions in the following link to work with them. https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html so you might have newtype (symbol :: Symbol) ::: value = Field value you can basically use any typelevel combinator you want for Sum e.g. ("foo" ::: Int) `(,)` ("bar" ::: Char) `(,)` ... or make your own You will have to use type families which are basically type level functions to merge two sums. If you run into trouble you can have a look at the following link which does some similar things. https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.h... P.S. Prepare for a headache Cheers Silvio
On Sat, Aug 15, 2015 at 02:35:53PM +0200, Silvio Frischknecht wrote:
I'm not going to do the whole thing for you but I can help start you off.
The type level string you think of is called Symbol. Symbol is a kind on it's own and not (*) it has a type for every string. You can use the functions in the following link to work with them.
https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html
so you might have
newtype (symbol :: Symbol) ::: value = Field value
you can basically use any typelevel combinator you want for Sum e.g.
("foo" ::: Int) `(,)` ("bar" ::: Char) `(,)` ...
or make your own
You will have to use type families which are basically type level functions to merge two sums.
If you run into trouble you can have a look at the following link which does some similar things.
https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.h...
P.S. Prepare for a headache
A good headache or a bad headache? If it's hard to learn but ultimately satisfying and useful then I'm all up for it. If it's hard to learn because Haskell doesn't really support it naturally then I'll probably avoid it. Tom
it is not a nice headache; doing quasi dependent types ends with lots of redundancy like implementing functions both at the type level and the value level, duplicating data types definitions (even though singletons helps there) If you want to learn more about dependent types, looking at Idris or Agda is what you actually want. I would avoid it, Haskell's type system is not a nice programming language to work with On Aug 15, 2015 10:13 AM, "Tom Ellis" < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:
On Sat, Aug 15, 2015 at 02:35:53PM +0200, Silvio Frischknecht wrote:
I'm not going to do the whole thing for you but I can help start you off.
The type level string you think of is called Symbol. Symbol is a kind on it's own and not (*) it has a type for every string. You can use the functions in the following link to work with them.
https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html
so you might have
newtype (symbol :: Symbol) ::: value = Field value
you can basically use any typelevel combinator you want for Sum e.g.
("foo" ::: Int) `(,)` ("bar" ::: Char) `(,)` ...
or make your own
You will have to use type families which are basically type level functions to merge two sums.
If you run into trouble you can have a look at the following link which does some similar things.
https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.h...
P.S. Prepare for a headache
A good headache or a bad headache? If it's hard to learn but ultimately satisfying and useful then I'm all up for it. If it's hard to learn because Haskell doesn't really support it naturally then I'll probably avoid it.
Tom _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
I would avoid it, Haskell's type system is not a nice programming language to work with
Do you know why this is so? And why dependent types are such a problem in Haskell? I've been wondering this for a while. Is it a GHC (System FC) problem or generally a Haskell problem? Or is it just that nobody really knows how dependent types are supposed to work anyway, so it's all a bit best effort? Or does it have something to do with inferring types and choosing instances. P.S. I'm more interested in practical problems or examples than a mathematical proof of why one type system is incompatible with another. Silvio
On Aug 18, 2015, at 12:52 PM, Silvio Frischknecht
I would avoid it, Haskell's type system is not a nice programming language to work with
Do you know why this is so?
Here's my take: the type-level programming features have been added one-at-a-time, without a coherent attempt to make a "type-level programming language". So it's missing some niceties, like case statements in type family definitions and local definitions. Some of these are easier to add than others. (Actually, the two I've listed here wouldn't be bad. Lambda is another story, though.)
And why dependent types are such a problem in Haskell?
No existing dependently typed language can infer the type of `length` from its body. But a dependently typed Haskell must do so. From a practical standpoint, GHC is just really big. And adding dependent types is a pervasive change that takes a *lot* of time. My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.) The bottom line: there is reason to hope that Haskell will have dependent types within the next two years or so. Richard
My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)
It's always nice to see things are happening. GHC is awesome. The thing with the star also being a typeoperator is a bit unfortunate. I always thought it a bit inconsistent to use an operator lexem for typekind even though it's not an operator at all. A normal name would have done.
The bottom line: there is reason to hope that Haskell will have dependent types within the next two years or so.
What exactly does that mean? The ability to use normal functions, Ints and Strings at typelevel, instead of type families, Nats and Symbols. or Just have a type-level language that is similar to the commonly used type dependent languages. Silvio
On Aug 19, 2015, at 4:54 PM, Silvio Frischknecht
My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)
It's always nice to see things are happening. GHC is awesome.
The thing with the star also being a typeoperator is a bit unfortunate. I always thought it a bit inconsistent to use an operator lexem for typekind even though it's not an operator at all. A normal name would have done.
Agreed completely. But that backward-compatibility nightmare that this change would cause just isn't worth it.
The bottom line: there is reason to hope that Haskell will have dependent types within the next two years or so.
What exactly does that mean?
The ability to use normal functions, Ints and Strings at typelevel, instead of type families, Nats and Symbols.
or
Just have a type-level language that is similar to the commonly used type dependent languages.
While I'm not sure what will happen with Nat/Symbol vs Int/String yet, I am hoping that functions will just be able to be used in types. We'll see how it all works out. But I'm aiming more for the first description than the second. As for timing: finishing an unpolished, not-ready-to-merge but functional implementation is part of my dissertation. I'm very much hoping to graduate by next summer, so there is a big incentive for me to actually get this done! Richard
A good headache or a bad headache? If it's hard to learn but ultimately satisfying and useful then I'm all up for it. If it's hard to learn because Haskell doesn't really support it naturally then I'll probably avoid it.
Well that depends on how you look at it. GHC has a fair number of extensions for dealing with type level programming. And there surely is a reason for all of them. And you can get some elegant type level programming. But it's hard to get right. It's is especially hard if you want Haskell to infer your types. It can definitely be worth it. I coded a unit system the day before yesterday. I'm using it in my project now and that was definitely worth it. But I've done stuff like this before and it usually takes a few days for me to wrap my head around things. Btw. I'm just an enthusiast. I don't do this professionally. I can tell you the extensions you will probably need and that you should have a look at. TypeFamilies - often useful (closed type families for defaults) KindSignatures - for working with different kinds such as Symbol TypeOperators - for making typelevel operators DataKinds - If you want to make your own kinds (probably not needed) Silvio
In Vivid 0.2 (out any day now!) I use type strings pretty pervasively. I'd say that for my needs they were really useful, but the design phase was long (and kinda painful). I can imagine many cases where they're too painful and/or not powerful enough but I'm very happy with what I ended up with.
A-, would type string again.
tom
El Aug 15, 2015, a las 9:35, Silvio Frischknecht
A good headache or a bad headache? If it's hard to learn but ultimately satisfying and useful then I'm all up for it. If it's hard to learn because Haskell doesn't really support it naturally then I'll probably avoid it.
Well that depends on how you look at it. GHC has a fair number of extensions for dealing with type level programming. And there surely is a reason for all of them. And you can get some elegant type level programming. But it's hard to get right. It's is especially hard if you want Haskell to infer your types. It can definitely be worth it. I coded a unit system the day before yesterday. I'm using it in my project now and that was definitely worth it. But I've done stuff like this before and it usually takes a few days for me to wrap my head around things.
Btw. I'm just an enthusiast. I don't do this professionally.
I can tell you the extensions you will probably need and that you should have a look at.
TypeFamilies - often useful (closed type families for defaults) KindSignatures - for working with different kinds such as Symbol TypeOperators - for making typelevel operators
DataKinds - If you want to make your own kinds (probably not needed)
Silvio _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
On Friday, August 14, 2015, Tom Ellis < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:
For the type level gurus:
I would like to define types
Sum :: [Field] -> *
(:::) :: String -> * -> Field
used like this
Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]
(I hope this makes sense. I'm not quite familiar with the syntax.)
such that
Sum '[ s1 ::: a1, ... ]
unifies with
Sum '[ s1 ::: b1, ... ]
to give
Sum '[ s1 ::: c1, ... ]
where c1 is the unification of a1 and b1. If sn is absent from exactly one of the unificands then its type is copied over unchanged. If sn is absent from both then it is absent from the unification. The types should also be invariant under permutation of the list.
This is perhaps a bit obscure so I'll explain the application. This is intended for the sumtype equivalent of a record type, so if we have
Sum '[ "foo" ::: a, "bar" ::: b ]
and
Sum '[ "foo" ::: a, "baz" ::: c ]
then I take take the sum of these sums and get something of type
Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]
If it makes it easier than I am happy for
Sum '[ s1 ::: a1, ... ]
to unify with
forall ak. Sum '[ s1 ::: a1, ..., sk ::: ak ]
This is justified by
forall b. Either a b
being isomorphic to a.
Is such a type possible? If so my next question will be about how to type deconstructors of such things, but let's start with a small first step!
Thanks,
Tom
This won't get you everything you mention out of the box, but I expect you can piece together the last bits of what you want with the exception that type inference will be limited. Here are basic open sums, conversions between sums and products, and matching against sums: http://hackage.haskell.org/package/Frames-0.1.2.1/docs/Frames-CoRec.html I make rather heavy use of this kind of programming, and have thus far found it to scale up quite well. Anthony
participants (6)
-
amindfv＠gmail.com -
Anthony Cowley -
Esteban I. RM. -
Richard Eisenberg -
Silvio Frischknecht -
Tom Ellis