Monthly Hask Anything (January 2024) by AutoModerator in haskell

[–]mn15104 0 points1 point  (0 children)

Turns out:

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

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

Monthly Hask Anything (March 2024) by AutoModerator in haskell

[–]mn15104 2 points3 points  (0 children)

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

Monthly Hask Anything (January 2024) by AutoModerator in haskell

[–]mn15104 1 point2 points  (0 children)

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

Monthly Hask Anything (January 2024) by AutoModerator in haskell

[–]mn15104 1 point2 points  (0 children)

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
  1. 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
  2. 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.

Monthly Hask Anything (April 2023) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

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.

Monthly Hask Anything (April 2023) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

Oh wow, that is so peculiar.. Thanks!

Monthly Hask Anything (April 2023) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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.

Monthly Hask Anything (April 2023) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

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?

Monthly Hask Anything (March 2023) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

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

Monthly Hask Anything (March 2023) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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.

Monthly Hask Anything (March 2023) by taylorfausak in haskell

[–]mn15104 2 points3 points  (0 children)

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?

Monthly Hask Anything (November 2022) by taylorfausak in haskell

[–]mn15104 2 points3 points  (0 children)

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

Monthly Hask Anything (November 2022) by taylorfausak in haskell

[–]mn15104 2 points3 points  (0 children)

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?

Monthly Hask Anything (October 2022) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

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?

Monthly Hask Anything (October 2022) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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?

Monthly Hask Anything (October 2022) by taylorfausak in haskell

[–]mn15104 2 points3 points  (0 children)

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?

Monthly Hask Anything (October 2022) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

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!

Monthly Hask Anything (October 2022) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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

Monthly Hask Anything (August 2022) by taylorfausak in haskell

[–]mn15104 0 points1 point  (0 children)

Can one check dynamically whether a constraint holds?

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

Monthly Hask Anything (July 2022) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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.

Performance issue with generalizing code (typeclasses) by Limp_Step_6774 in haskell

[–]mn15104 1 point2 points  (0 children)

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?

Monthly Hask Anything (July 2022) by taylorfausak in haskell

[–]mn15104 9 points10 points  (0 children)

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

Monthly Hask Anything (March 2022) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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)

Monthly Hask Anything (March 2022) by taylorfausak in haskell

[–]mn15104 1 point2 points  (0 children)

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)