Type families vs data families vs GADTs - Haskell

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

Bolt

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?

TheMatten

@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 = ...
Bolt

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

TheMatten

@Bolt maybe describing what's your final goal could be helpful :slight_smile:

Bolt

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!

TheMatten

Problem is that division on Nats would be partial

Bolt

Type families allow me to do this ?

Bolt

It's fine to define something that truncates at 0

Bolt

and it's also fine to it to floor/ceil the result

TheMatten

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
Bolt

Can you please explain me what is a closed type family and the reason of the comment and the r -> n m bit?

Bolt

what annotation are you referring to?

TheMatten

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

TheMatten

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"

TheMatten

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

Bolt

ohh okay! thank you very much!

Bolt

When you say that in the case of open type families the cases can't overlap what do you mean exactly?

Bolt

can you give a concrete example? I'm having a hard time figuring out

Bolt

Also the D type familie isn't a type is it? Can I use it to derive instances? (sorry for my newbness :sweat_smile: )

TheMatten
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
    |               ^^^^^^^
TheMatten

If you say Foo Int Bool, which one should it choose?

Bolt

ohh got it! thanks :D

TheMatten

D n m e is a type in a same way head [1] is a value - they're applied functions

TheMatten

You can't derive instances on it directly - one simple reason is that we can't have type families in instance heads yet

TheMatten

(NP, I was learning to use them at some point too :smiley:)

Bolt

okay so I have to play with E and B types only

Bolt

so, now to define the division I need to use a type family as well right?

TheMatten

Yeah - you can try writing it first at value level, without using case, if or guards

Bolt

Okay! Thanks for the tip! :D

Bolt

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)

Bolt

Here is only declared the family

Lysxia

It's part of the compiler

Lysxia

There is no in-library definition

Bolt

oh okay! Thanks!

Bolt

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?

Bolt

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
Alexis King

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

Bolt

I want it to be habited. I understand the reason for it not to be habited

Alexis King

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.

Alexis King

What does a value of type Test n m mean/why would you like Test 3 3 to be inhabited?

Bolt

Just a brain teaser

Bolt

I feel like it is possible but I dont know how to do it!

Alexis King

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. :)

Bolt

I want to be able to have a value that is of type T 3 m for example

Alexis King

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?

Bolt

yes, but how can I change the definition of Test to be able to have what I want?

Alexis King

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

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

TheMatten

@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

Bolt

Can I have some kind of overlapping?

Alexis King

I’d do it this way:

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

Like

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

@Alexis King Probably depends on usecase

Alexis King

Yes, agreed. In a dependently typed language the tradeoffs would be different.

Bolt

I'll try all of your suggestions!

Bolt

Thanks for the help, I feel like I'm learning to program for the first time ahaha

Sandy Maguire

For things like this, GADTs are more often what you want than data families

Bolt

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

TheMatten

@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

Bolt

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

TheMatten

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
TheMatten

I still wonder whether it would be sound to have some "unguarded" existential quantifier in Haskell - forsome n m. T n m

Bolt

Can I do that with my existent GADT?

Bolt

Getting things to compile

Bolt

I'm going with a type family approach mixed with GADTs now and test it

TheMatten

Do that CPS style as above for example - take continuation and pass resulting T into it

Bolt

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

Bolt

is that possible?

TheMatten

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

Bolt

okay, cool! Thanks!

TheMatten

(You need ConstraintKinds for first one BTW)

Bolt
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
TheMatten

@Bolt What's the code?

Bolt
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
TheMatten

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

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

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

Bolt

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

TheMatten

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

Bolt

Are you saying it is possible to solve my problem?

TheMatten

In Core this would be more apparent

TheMatten

Basically, if you want to pass concrete T around, you have to hide it's arguments in existential wrapper/context - then it will work

TheMatten

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

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

Bolt

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

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

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

TheMatten

@Bolt KnownDimensions n m is (KnownNat n, KnownNat m)?

TheMatten

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

Bolt

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

Lysxia

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

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

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

Sandy Maguire

@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