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! 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? 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` 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
|               ^^^^^^^
``` You can't derive instances on it directly - one simple reason is that we can't have type families in instance heads yet Yeah - you can try writing it first at value level, without using `case`, `if` or guards 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)? 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? 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. :) 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`? 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
``` @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 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` I know but how to wrap them on a single name like `Myconstraint = (a,b,c)` and then I can use it `g :: Myconstraint => ...` 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 ```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
``` ```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
``` ```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
``` 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 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? ```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)? 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  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` 