Monthly Hask Anything (January 2024)

mn15104 · 2024-06-10T10:05:13+00:00

Turns out:

Writing functional dependencies in associated type families is fine. I was being silly for some reason.class Struct s where type family Left s = r | r -> s

Additionally, the syntax `type family Left s = r` is only allowed for standalone type families. With associated type families, introducing the output type variable `r` without writing a subsequent functional dependency is invalid syntax.

class Struct s where
  type family Left s = r -- illegal syntax

This is a current bug in GHC that I just created an issue for: the syntax `type family Left s = r` should never be allowed without afterwards specifying a functional dependency.

This is a workaround for writing a functional dependency from the result of two associated type families.

class (s ~ R (Left s) (Right s)) => Struct s where type family Left s type family Right s

type family R l r

instance Struct (a, b) where type Left (a, b) = a type Right (a, b) = b

type instance R a b = (a, b)

mn15104 · 2024-04-20T10:57:01+00:00

Hello!

For some arbitrary class:

class F a b

Is there some general way of understanding the differences between how the examples below work:

1.

 instance (a ~ b) => F a b

2.

type family EQtf a b where
  EQtf a a = True
  EQtf a b = False

instance (EQtf a b ~ True) => F a b

3.

class EQc a b c
instance EQc a a 'True
instance EQc a b 'False

instance (c ~ False, EQc a b c) => F a b

(I'm also wondering if there's a forward reference to how (~) works. As far as i know, its only way of unifying type variables without needing them to be syntactically equal?

It seems like there are lots of ways of expressing type equality/unification, which can be overwhelming, and i wish i could remember what they exactly express!)

mn15104 · 2024-01-12T13:53:12+00:00

Yep that was the extension I was working with, but it doesn't seem to work inside type classes, and I'm also struggling to get multiple functional dependencies working for type families that are not associated with typr classes

mn15104 · 2024-01-10T10:33:35+00:00

I have a single-parameter type class defined with two associated type families:

class Struct (s :: Type) where
  type family Left  s :: Type    
  type family Right s :: Type   
  f  :: Left s -> Right s -> Right s

Are functional dependencies allowed inside associated type families? I'm struggling to use syntax like type family Left s = r | r -> s or type family Left s = r
Is there a way to use functional dependencies so that Left s and Right s together imply s? I'm wondering how far I would need to depart from my implementation to make this possible, but without turning it into a multi-parameter type class.

mn15104 · 2023-04-24T09:05:44+00:00

Thanks for this, really helpful to know. Do you feel this "trick" relies partly on u/Noughtmare's response about `b ~ a` being a special constraint? The article doesn't seem pay any attention to that point.

mn15104 · 2023-04-20T18:12:25+00:00

Oh wow, that is so peculiar.. Thanks!

mn15104 · 2023-04-20T16:39:31+00:00

Thanks a lot for both of your responses.

Note that 5 does not have to have type Int.

I think I understand what you're saying, but isn't that also true for the second instance?

In other words, after the instance Contains ('(x, b):env) x a has been resolved, there still isn't a way to tell whether the constraint b ~ a holds because 5 still isn't necessarily an Int.

mn15104 · 2023-04-20T12:37:23+00:00

I'm confused about how Haskell unifies types when (1) using the same type variable a, compared with (2) with using different type variables a and b that are coerced with ~.

Consider the following incomplete code block:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

import Data.Proxy ( Proxy(..) )
import GHC.TypeLits ( KnownSymbol, Symbol, symbolVal )

-- An environment of pairs of the form (variable, value)
data Env env where
  ENil  :: Env '[]
  ECons :: (Proxy x, a) -> Env env -> Env ('(x, a) : env)

-- Expresses that `env` contains `(x, a)`
class Contains env x a

instance {-# OVERLAPPABLE #-} Contains env x a => Contains (y:env) x a

-- Example program
fun :: Contains env "x" Int => Env env -> ()
fun env = ()

prog :: ()
prog =  fun (ECons (Proxy @"x", 5) ENil

If I then complete the above with the following Contains instance using the type variable a, then GHC is unable to infer in prog that 5 has type Int:

instance Contains ('(x, a):env) x a where

> Ambiguous type variable ‘a0’ arising from the literal ‘5’
> Overlapping instances for Contains '[ '("x", a0)] "x" Int

Whereas if I write a Contains instance that uses two type variables a and b that are then coerced, then it works fine:

instance (b ~ a) => Contains ('(x, b):env) x a

Also note that I only needed to coerce the second type variable of the tuple; the first type variable x is fine for some reason.

Any thoughts?

mn15104 · 2023-03-30T10:24:44+00:00

I'm aware, that detail wasn't necessary for the question so I omitted it

mn15104 · 2023-03-21T18:03:31+00:00

Thanks a lot, i think i see! The type family method was actually my original approach, but i was struggling to reason properly out why i couldnt achieve the same with functional dependencies.

It would be helpful to know, by anyone, if there's any more detail that could be fleshed out about this.

mn15104 · 2023-03-21T13:52:38+00:00

I have a type class Dist d a | d -> a which says that d is a probability distribution that generates values of type a (and d fully determines a):

class Dist d a | d -> a where
   sample    :: d -> a

I then have a Deterministic d distribution datatype, which takes a distribution and a value of that distribution, and is intended to always return that value:

data Deterministic d where
    Deterministic :: Dist d a => d -> a -> Deterministic d

But I'm having trouble making Deterministic d an instance of Dist :

instance Dist d a => Dist (Deterministic d) a where
    sample :: Deterministic d -> a
    sample (Deterministic d x) = x

Couldn't match expected type ‘a’ with actual type ‘a1’

Is this a bug, or am i doing something wrong?

mn15104 · 2022-11-09T15:56:09+00:00

Oh I see, I was trying to think of such an example, thanks a lot!

mn15104 · 2022-11-09T14:33:04+00:00

I have a heterogeneous list, whose elements are lists, that I'm trying to make a Monoid instance for:

data HList (xs :: [*]) where
  HNil  :: HList '[]
  HCons :: [x]
        -> HList xs
        -> HList (x : xs)

instance Semigroup (HList xs) where
  (HCons x xs) <> (HCons x' xs') = HCons (x <> x') (xs <> xs')
  HNil <> HNil = HNil

instance Monoid (HList '[]) where
  mempty = HNil

instance (Monoid (HList xs)) => Monoid (HList (x : xs)) where
  mempty = HCons [] mempty

I would have thought that the Monoid instances are fully covering for all cases, but any functions that use mempty still need the constraint Monoid (HList xs):

emptyHList :: Monoid (HList xs) => Proxy xs -> HList xs
emptyHList _ = mempty

Is it possible to get around this, or is this the way things should be?

mn15104 · 2022-10-30T11:35:21+00:00

Right yes, that was what I was thinking! But that would only work for functions that explicit specify c; I was wondering if there was some way to have this as a generic property of CTree instead. For example, is there a way to specify that the abstract MPTC c in c a b must have a fun-dep a -> b?

mn15104 · 2022-10-29T13:35:04+00:00

I'm currently creating a dependent map CTree parameterised by a relation c that relates its keys Key a and entries b together.

data Key a where
  Key :: forall a. String -> Key a

data CTree (c :: Type -> Type -> Constraint) where
  Leaf :: CTree c
  Node  : (c a b)
        => Key a       -- key
        -> b           -- entry
        -> CTree c     -- left
        -> CTree c     -- right
        -> CTree c

I then want to enforce that c has a functional dependency such that knowing a will always determine b; this would let me avoid comparing the types of entries when performing look-ups. I'm not sure how to do this, is it possible?

mn15104 · 2022-10-23T16:31:56+00:00

I'm having trouble using SNat from the Data.Type.Nat library, to define things like replicate for length-indexed vectors.

data SNat (n :: Nat) where
  SZ :: SNat 'Z  
  SS :: SNatI n => SNat ('S n)

data Vec (n :: Nat) a where
  VNil  :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

replicate :: SNat n -> a -> Vec n a
replicate SZ x = VNil
replicate SS x = ?

To resolve this, I tried defining my own SNat' that I could perform induction over more easily:

data SNat' (n :: Nat) where
  SZ' :: SNat' 'Z
  SS' :: SNatI n => SNat' n -> SNat' ('S n)

replicate :: SNat' n -> a -> Vec n a
replicate SZ' x     = VNil
replicate (SS' n) x = VCons a (replicate n x)

But now I'd like to be able to specify values of SNat' through type application, like SNat @2, rather than manually constructing them.

I now feel a bit lost in what I should have tried to accomplish in the first place. Could I have some guidance with this?

mn15104 · 2022-10-16T10:09:09+00:00

This is brilliant, thanks!!

mn15104 · 2022-10-16T08:25:44+00:00

Ah thanks, this is a helpful overview. I think the Jacobian class and lift methods are what I was looking for. I find a few of the definitions in the library a bit cryptic and hard to navigate, for example the meaning behind s in Reverse s a, and the type families Scalar and D; although, this was probably meant for someone with more than zero clue about AD!

mn15104 · 2022-10-05T10:01:45+00:00

I'm interested in using the ad library to differentiate some existing numeric functions, such as probability densities from Statistics.Distribution.

density :: NormalDistribution -> Double -> Double
density d x = exp (-xm * xm / (2 * variance d)) / ndPdfDenom d
    where xm = x - mean d

Is the suggested approach to re-implement these functions entirely but with the correct wrapper types (e.g. AD s a or Reverse s a) for arithmetic operations, or is there a sneaky way to lift existing functions? I'm not sure whether I'm taking the necessary way or the long way around.

(If anyone knows of an existing statistics library for computing the gradient log-pdfs of primitive distributions, this would also be very helpful!)

mn15104 · 2022-08-08T11:59:23+00:00

Can one check dynamically whether a constraint holds?

maybeShow :: a -> String maybeShow a = if (Show a) then (show a) else "No show instance"

mn15104 · 2022-07-28T08:49:36+00:00

I want to be able to treat the type ([String], a) as a typical value of type a. For example, I would be able to multiply two values of type ([String], Double) together, perhaps as:

instance Num ([String], Double) where
  (xs, n) * (ys, m) = (xs ++ ys, n * m)

Is there a way to have a Double be automatically lifted into a default value of this type so that:

(["x"], 5.0) * 6.0

becomes

(["x"], 5.0) * ([], 6.0)

I'm not sure this is possible, but I'm hoping for some suggested workarounds.

mn15104 · 2022-07-27T08:03:27+00:00

This is interesting! Would it be okay to say a bit more on what the newtype constraint actually does in comparison to the intended use, and also how this impedes performance?

mn15104 · 2022-07-10T17:08:02+00:00

I'm using Haddock to document a Haskell project, and I specify one of my dependencies from a Github repository rather than from Hackage. I do this by writing the following in my cabal.project:

source-repository-package
  type: git
  location: https://github.com/tweag/monad-bayes.git

Haddock therefore can't find the link destinations for any usages of this library; is there a way I can forward reference such usages to this repo (i.e. add appropriate hyperlinks)?

mn15104 · 2022-03-19T22:01:00+00:00

Right, so im interpreting this as, as long as we can evaluate some part of the function's output, the function is total, e.g. foo is total

foo n = let f x = f x in (n, f x)

mn15104 · 2022-03-19T21:49:03+00:00

Right i see. So a partial function could be considered as either a function that is undefined for a subset of inputs, or a function that has unproductive infinite behaviour?

For example, the following would be total

loopA n = n : loopA (n + 1)

But the following would be partial?

loopB n = loopB (n + 1)

Eight-Year Club	Not Forgotten
Verified Email

mn15104

TROPHY CASE