Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

How can I define a type safe inductive data type like

```data D 1 1 e = E e
data D (n :: Nat) (m :: Nat) e = ...
```

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`:

```data D :: Nat -> Nat -> Type where
E :: e -> D 1 1 e
...
```

for extensible type you can use data families:

```data family D :: Nat -> Nat -> Type
data instance D 1 1 e = E e
data instance D n m e = ...
```

I think type families are what I want! Because in the inductive case I don't want something different than `E e`

Something like this:

```data D 1 1 e = E e
data D (n :: Nat) (m :: Nat) e = D (B n m e)

data B (n :: Nat) (m :: Nat) e = S (D (n/2) m e) | J (D n (m/2))
```

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 partial

Type 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` to `D` data constructor, you want to use closed type family:

```newtype E e = E e
data    B (n :: Nat) (m :: Nat) e = S (D (n / 2) m e) | J (D n (m / 2) e)

-- This seems to be injective, let's try putting annotation here
type family D (n :: Nat) (m :: Nat) e = r | r -> n m where
D 1 1 e = E e
D n m e = B n m e
```

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:

```type family D n m e

type instance D 1 1 e = E e
type instance D n m e = B n m e
```

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 know `r`" (as in result), "I know `n` and `m` 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 to `D 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: )

```type family Example a b

type instance Example Int b    = Int
type instance Example a   Bool = Bool
```
```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
|               ^^^^^^^
```

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 way `head [1]` is a value - they're applied functions

You 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` and `B` types only

so, 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 guards

Okay! 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

```data Test (n :: Nat) (m :: Nat) where
C :: Test (Div n 2) m -> Test (Div n 2) m -> Test n m
O :: Test 1 1
```

I cannot construct something of type `Test 3 3` how can I solve this?

I get the following error when trying

```Couldn't match type ‘0’ with ‘1’
Expected type: Test (Div 1 2) 1
Actual type: Test 1 1
```

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)?

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 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`.

What does a value of type `Test n m` mean/why would you like `Test 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 to `Test` that is `A :: 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 example

Do you follow my above reasoning as to why, given that definition of `Test`, `Test n m` can only be inhabited when `m` is `1`?

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 all `m`, you could just add another case to `Test` with type `Test 3 m`, like this:

```data Test (n :: Nat) (m :: Nat) where
C :: Test (Div n 2) m -> Test (Div n 2) m -> Test n m
O :: Test 1 1
A :: Test 3 m
```

I want to be able to construct any T for which 'n' is Odd

@Bolt

```data T n m where
C :: Odd n => T n m
```

Where `Odd` is a typeclass or a synonym for some type family equality

Can I have some kind of overlapping?

I’d do it this way:

```data T n where
One :: T 1
Next :: T n -> T (n + 2)
```

Like

```data T n m where
C :: Odd n => T n m
C :: Even n => ...
```

@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

```Couldn't match type ‘n’ with ‘1’
‘n’ is a rigid type variable bound by
the type signature for:
g :: forall (n :: Nat) (m :: Nat).
Integer -> Integer -> T n m
at <interactive>:2:1-39
Expected type: T n m
Actual type: T 1 1
```

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` 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

But why can't `T 1 1` be inferred as `T n m`? :confused: Is there any way to achieve this?

You want some existential wrapper or CPS probably:

```data SomeT = forall n m. SomeT (T n m)
```
```g :: Integer -> Integer -> (forall n m. T n m -> r) -> r
```

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?

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 it

How 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 it `g :: 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)

```Couldn't match type ‘T n1 m1’ with ‘T n m’
Expected type: T n1 m1 -> T n m
Actual type: T n m -> T n m
NB: ‘T’ is a non-injective type family
```

@Bolt What's the code?

```el :: e -> T 1 1
el = E

zeros :: forall e n m . (Zero e, KnownDimensions n m) => T n m
zeros = let c = natVal (Proxy :: Proxy n)
r = natVal (Proxy :: Proxy m)
in go c r id
where
go :: Integer -> Integer -> (forall e n m . (Zero e, KnownDimensions n m) => T n m -> r) -> r
go 1 1 c = c (el zero)
go n m c = undefined
```

How does `T` look like?
`go c r id` won't work - for the same reason you're using CPS

```data T (c :: Nat) (r :: Nat) where
J :: (ValidDimensions m p, ValidDimensions n p) => T m p -> T n p -> T (m + n) p
S :: (ValidDimensions p m, ValidDimensions p n) => T p m -> T p n -> T p (m + n)
One :: T 1 1
```

Why can't `T 1 1` be inferred as `forall n m . T n m` ?? That sounds stupid to me

How can I be polymorphic in `One` type constructor but still have it return `T 1 1` ?

That would be like saying `(1, 1) = \a b -> (a, b)` - `forall n m. T n m` is basically an implicit type function

Are 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 work

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

```data T (c :: Nat) (r :: Nat) where
J :: (ValidDimensions m p, ValidDimensions n p) => T m p -> T n p -> T (m + n) p
S :: (ValidDimensions p m, ValidDimensions p n) => T p m -> T p n -> T p (m + n)
One :: T 1 1

data TWrapper = forall n m . TW (T n m)
```

like this?

But that way Im going to loose the type safety on the Natural numbers :confused:

```el :: T 1 1
el = One

zeros :: forall e n m . (Zero e, KnownDimensions n m) => T n m
zeros = let c = natVal (Proxy :: Proxy n)
r = natVal (Proxy :: Proxy m)
(TW t) = go c r
in t
where
go :: Integer -> Integer -> TWrapper
go 1 1 = TW el
go n m = undefined
```

I'm trying this and get

```Couldn't match type ‘n1’ with ‘n’
‘n1’ is a rigid type variable bound by
a pattern with constructor:
TW :: forall e (n :: Nat) (m :: Nat). T n m -> TWrapper,
in a pattern binding
```

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)`?

I would probably consider doing this using typeclass:

```class Zeros n m where
zeros :: T n m
```

this way you easily avoid problems with known indexes and plus it should inline nicely when `n` and `m` are known at call site

Im not sure I understand, will that solve my problem?

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`