@Bolt If you want to be able to pattern match on type with any arguments and want type to be at least partially inferable from data constructors, you can use GADTs:
Okay, let's assume we have integer division - because you surely don't want to ever map D 1 1 to D data constructor, you want to use closed type family:
newtypeEe=EedataB(n::Nat)(m::Nat)e=S(D(n/2)me)|J(Dn(m/2)e)-- This seems to be injective, let's try putting annotation heretypefamilyD(n::Nat)(m::Nat)e=r|r->nmwhereD11e=EeDnme=Bnme
error:
Conflicting family instance declarations:
Example Int b = Int -- Defined at experiments.hs:513:15
Example a Bool = Bool -- Defined at experiments.hs:514:15
|
513 | type instance Example Int b = Int
| ^^^^^^^
What is Test intended to capture? Given the definition provided, Test 3 3 doesn’t seem like it ought to be inhabited to me. It isn’t O, trivially, and you can’t get it from C, because that would require a value Test (Div 3 2) 3, and Div 3 2 is bottom (since 3/2 is not a natural number). Is there a particular reason you think it ought to be inhabited (or perhaps would like it to be inhabited)?
Oh, I see—Div 3 2is defined, my bad. It just rounds down to 1. But then you would need a value of type Test 1 3, at which point you would need a value of type Test (Div 1 2) 3 to get it, and Div 1 2 is 0, so then you need a value of type Div 0 3… and so on. It will never be inhabited because m is always 3, and the only base case for Test pins m to be 1.
Well, I ask because it is trivial to make Test 3 3 be inhabited by adding a case to Test that is A :: Test 3 3, but presumably you do not want that solution. :)
Well, I’m still not quite sure I understand what you want, I guess. If you want Test 3 m to be inhabited, for all m, you could just add another case to Test with type Test 3 m, like this:
@Bolt Look at it this way - return type of g is T n m, where I as a caller should be able to choose n and m, but you're trying to return T 1 1 specifically in that case
Two ways:
- type synonym type Foo = (Bar, Baz)
- class synonym class (Bar, Baz) => Foo; instance (Bar, Baz) => Foo
second option has advantage of being partially applicable if it has arguments
Because basically the only possible direct quantification in Haskell is universal - and universal one assumes that you can actually put any arguments in there as a caller
Real dependent types are coming to Haskell soon! Until then, we have the great singletons library :) If you’ve ever run into dependently typed programming in Haskell, you’ve probably encountered mentions of singletons (and the singletons library). This series of articles will be my attempt at giving you the story of the library, the problems it solves, the power that it gives to you, and how you can integrate it into your code today! (Also, after my previous April Fools post, people have been asking me for an actual non-joke singletons post) This post (Part 1) will go over first using the singleton pattern for reflection, then introducing how the singletons library helps us. Part 2 will discuss using the library for reification, to get types that depend on values at runtime. Part 3 will go into the basics of promoting functions values to become functions on types in a usable, and Part 4 will go deeper into the lifting of functions, using singleton’s defunctionalization scheme to utilize the higher-order functions we love at the type level. Part 3 will go into the basics singleton’s I definitely am writing this post with the hope that it will be obsolete in a year or two. When dependent types come to Haskell, singletons will be nothing more than a painful historical note. But for now, singletons might be the best way to get your foot into the door and experience the thrill and benefits of dependently typed programming today!
@Bolt can you share the whole code with me? i'm lost trying to piece it together from the conversation, but I'm pretty sure there is a silly mistake being made here somewhere
How can I define a type safe inductive data type like
I hope you get the idea, I'm not familiar with the type level machinery is this possible?
@Bolt If you want to be able to pattern match on type with any arguments and want type to be at least partially inferable from data constructors, you can use
GADTs
:for extensible type you can use data families:
I think type families are what I want! Because in the inductive case I don't want something different than
E e
@Bolt maybe describing what's your final goal could be helpful :slight_smile:
Something like this:
Where
n/2
would be some kind of operation on the kind Nat that divides the number by two!Problem is that division on
Nat
s would be partialType families allow me to do this ?
It's fine to define something that truncates at 0
and it's also fine to it to floor/ceil the result
Okay, let's assume we have integer division - because you surely don't want to ever map
D 1 1
toD
data constructor, you want to use closed type family:Can you please explain me what is a closed type family and the reason of the comment and the
r -> n m
bit?what annotation are you referring to?
Ah, sorry :sweat_smile::
- closed type family cannot be extended, but it's cases are matched in order - on the other hand, open type families:
can be extended, but their cases can't overlap
r -> n m
is that annotation - it's "type family dependency" and it basically says "if I knowr
" (as in result), "I known
andm
too"I put it here because it seems like I can - and because now by writing value
E something
, compiler can infer that it's type corresponds toD 1 1 e
ohh okay! thank you very much!
When you say that in the case of open type families the cases can't overlap what do you mean exactly?
can you give a concrete example? I'm having a hard time figuring out
Also the
D
type familie isn't a type is it? Can I use it to derive instances? (sorry for my newbness :sweat_smile: )If you say
Foo Int Bool
, which one should it choose?ohh got it! thanks :D
D n m e
is a type in a same wayhead [1]
is a value - they're applied functionsYou can't derive instances on it directly - one simple reason is that we can't have type families in instance heads yet
(NP, I was learning to use them at some point too :smiley:)
okay so I have to play with
E
andB
types onlyso, now to define the division I need to use a type family as well right?
Yeah - you can try writing it first at value level, without using
case
,if
or guardsOkay! Thanks for the tip! :D
How can I see the type family definition of
Nat
provided by GHC.TypeLit ? (https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.TypeNats.html#Div)Here is only declared the family
It's part of the compiler
There is no in-library definition
oh okay! Thanks!
If I have something like
I cannot construct something of type
Test 3 3
how can I solve this?I get the following error when trying
What is
Test
intended to capture? Given the definition provided,Test 3 3
doesn’t seem like it ought to be inhabited to me. It isn’tO
, trivially, and you can’t get it fromC
, because that would require a valueTest (Div 3 2) 3
, andDiv 3 2
is bottom (since 3/2 is not a natural number). Is there a particular reason you think it ought to be inhabited (or perhaps would like it to be inhabited)?I want it to be habited. I understand the reason for it not to be habited
Oh, I see—
Div 3 2
is defined, my bad. It just rounds down to1
. But then you would need a value of typeTest 1 3
, at which point you would need a value of typeTest (Div 1 2) 3
to get it, andDiv 1 2
is0
, so then you need a value of typeDiv 0 3
… and so on. It will never be inhabited becausem
is always3
, and the only base case forTest
pinsm
to be1
.What does a value of type
Test n m
mean/why would you likeTest 3 3
to be inhabited?Just a brain teaser
I feel like it is possible but I dont know how to do it!
Well, I ask because it is trivial to make
Test 3 3
be inhabited by adding a case toTest
that isA :: Test 3 3
, but presumably you do not want that solution. :)I want to be able to have a value that is of type
T 3 m
for exampleDo you follow my above reasoning as to why, given that definition of
Test
,Test n m
can only be inhabited whenm
is1
?yes, but how can I change the definition of
Test
to be able to have what I want?Well, I’m still not quite sure I understand what you want, I guess. If you want
Test 3 m
to be inhabited, for allm
, you could just add another case toTest
with typeTest 3 m
, like this:I want to be able to construct any T for which 'n' is Odd
@Bolt
Where
Odd
is a typeclass or a synonym for some type family equalitySo obvious!
Can I have some kind of overlapping?
I’d do it this way:
Like
@Alexis King Probably depends on usecase
Yes, agreed. In a dependently typed language the tradeoffs would be different.
I'll try all of your suggestions!
Thanks for the help, I feel like I'm learning to program for the first time ahaha
For things like this, GADTs are more often what you want than data families
I went with GADTs and am having this error
I'm trying to write a recursive function that in the base case returns something of type
T 1 1
@Bolt Look at it this way - return type of
g
isT n m
, where I as a caller should be able to choosen
andm
, but you're trying to returnT 1 1
specifically in that caseBut why can't
T 1 1
be inferred asT n m
? :confused: Is there any way to achieve this?You want some existential wrapper or CPS probably:
I still wonder whether it would be sound to have some "unguarded" existential quantifier in Haskell -
forsome n m. T n m
Can I do that with my existent GADT?
What exactly?
Getting things to compile
I'm going with a type family approach mixed with GADTs now and test it
Do that CPS style as above for example - take continuation and pass resulting
T
into itHow can I group a bunch of constraints into one?
@Bolt
(,)
I know but how to wrap them on a single name like
Myconstraint = (a,b,c)
and then I can use itg :: Myconstraint => ...
is that possible?
Two ways:
- type synonym
type Foo = (Bar, Baz)
- class synonym
class (Bar, Baz) => Foo; instance (Bar, Baz) => Foo
second option has advantage of being partially applicable if it has arguments
okay, cool! Thanks!
(You need
ConstraintKinds
for first one BTW)D:
@Bolt What's the code?
How does
T
look like?go c r id
won't work - for the same reason you're using CPSWhy can't
T 1 1
be inferred asforall n m . T n m
?? That sounds stupid to meHow can I be polymorphic in
One
type constructor but still have it returnT 1 1
?That would be like saying
(1, 1) = \a b -> (a, b)
-forall n m. T n m
is basically an implicit type functionAre you saying it is possible to solve my problem?
In Core this would be more apparent
Basically, if you want to pass concrete
T
around, you have to hide it's arguments in existential wrapper/context - then it will workBecause basically the only possible direct quantification in Haskell is universal - and universal one assumes that you can actually put any arguments in there as a caller
like this?
But that way Im going to loose the type safety on the Natural numbers :confused:
I'm trying this and get
So bottom line is there a way for GHC to don't be a bitch about specific types?
Doesn't it make sense for (1 :: Nat) to unify with (n :: Nat)?
@Bolt
KnownDimensions n m
is(KnownNat n, KnownNat m)
?Yes
I would probably consider doing this using typeclass:
this way you easily avoid problems with known indexes and plus it should inline nicely when
n
andm
are known at call siteIm not sure I understand, will that solve my problem?
Not a direct answer to your problem but it looks like you will be well served by reading about singletons. https://blog.jle.im/entry/introduction-to-singletons-1.html
The problem with my data type is that I cannot write a function that can build it because of the stupid base case
T 1 1
@Bolt can you share the whole code with me? i'm lost trying to piece it together from the conversation, but I'm pretty sure there is a silly mistake being made here somewhere
Yes!