I’m trying to use the vec package to implement a stack machine: Instructions are tagged with the number of their parmeters and return values, and the evaluator pops the parameters off the Vec stack, evaluates the instruction, and pushes the return values back.
The following code doesn’t compile:
import Data.Type.Nat
import Data.Vec.Lazy as Vec (Vec (..))
data ArithBlock (n :: Nat) (m :: Nat) where
eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int
eval = undefined
The error:
• Couldn't match type: Plus n x0
with: Plus n x
Expected: ArithBlock n m
-> Vec (Plus n x) Int -> Vec (Plus m x) Int
Actual: ArithBlock n m
-> Vec (Plus n x0) Int -> Vec (Plus m x0) Int
Note: ‘Plus’ is a non-injective type family.
The type variable ‘x0’ is ambiguous
• In the ambiguity check for ‘eval’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int
Note that vec uses the fin package for Natural numbers, which uses a Peano encoding, instead of GHC’s built-in literals. But ultimately I beleive they support the same set of operations (besides for GHC builtins getting better arithmetic logic via typechecker plugins, which I am trying to avoid)
I’m guessing the answer involves threading through a singleton for x, is there any way to avoid this?
The simple solution is to make x a required type argument. You can also try your luck at enabling AllowAmbiguousTypes, but maybe you’ll get an ambiguity error when you try to use eval anyway.
I do think Plus n (given one argument) should be injective. Perhaps you can find some other way to define it which the compiler can understand. For example a typeclass with functional dependencies.
AllowAmbiguousTypes will just push the logical problem elsewhere. A required type argument won’t help because x is highly dynamic.
There seems to be two possible approaches here:
Somehow get the compiler to understand the relationship between m, n and x in the way that it can work here. This is my preferece, but I’m open to the fact that it might not be possible.
Thread through a singleton for x. This is complicated by the fact that it is not trivial to know what x is at any given point. I think I will try implementing an algorithm that passes x in the dumb-list version of my machine.
People have traditionally solved this problem by passing proxy x arguments, but RequiredTypeArguments is the upgrade that makes such runtime proxies obsolete in recent GHCs.
It’s not clear to me exactly why you’re writing this approach off; dynamacy shouldn’t pose an issue. I suggest you try it and let us know what roadblocks you hit.
Not necessarily. If all the ArithBlocks have constants as arguments (e.g. ArithBlock (S (S Z)) (S Z)) then GHC can infer the ambiguous x without issues. Here’s a simplified example of that:
{-# LANGUAGE AllowAmbiguousTypes, TypeFamilies, DataKinds, RequiredTypeArguments #-}
data Nat = Z | S Nat
type family Plus x y where
Plus Z x = x
Plus (S x) y = S (Plus x y)
data Proxy a = Proxy
foo :: forall x y -> Proxy (Plus x z) -> Proxy (Plus y z)
foo _ _ Proxy = Proxy
bar = foo (S (S Z)) (S Z) Proxy -- not ambiguous
I didn’t narrow it down to something specific, but I dropped it as being trouble compared to Proxy for not much gain.
I expect my code to compile warning-free. When using variables introduced by forall n ->, I found trying to juggle the variables introduced in the type signature and in the pattern match, with type applications/inline type signatures, I seemed to always have either an undeclared or an unused variable. Something like, a function wouldn’t compile without a variable being included in forall n., but when I did include it, I got an unused type variable warning. I just gave up and switched to proxies.
Having said that, there is a feature of RequiredTypeArguments that I do like. Until now, the only way to go from type (or data kind) -> term was with a typeclass. this has the disadvantage of a) unwieldly syntax (for this use case) and b) It doesn’t support closed classes. By RTA allows me to pattern-match on types in function syntax, which is nice. So I may well come back to them someday and settle my differences properly.
Could you give an example of what you mean here? It sounds like you’re saying it’s possible to do something like this:
f :: forall (a :: Type) -> Int
f Int = 0
f Bool = 1
But that gives an error:
• Couldn't match expected type ‘a’ with actual type ‘Int’
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a -> Int
• In the pattern: Int
In an equation for ‘f’: f Int = 0
Right, RequiredTypeArgumentsdoesn’t allow you to do that. It’s just syntax. What will allow you to do that is foreach. I’ve no idea how long through the development pipeline that is. And in the meantime, the library feature that supports this functionality is singletons (whether with the singletons package specifically, or with the general notion).
No, matching on types is not (and should not be) possible even with full dependent types like in Agda. I hope this is not a planned feature.
What you would be able to do with full dependent types is create a data type and map that to the type level:
data MyType = TInt | TBool
typeOfMyType :: MyType -> Type
typeOfMyType TInt = Int
typeOfMyType TBool = Bool
negateLike :: foreach (t :: MyType) -> typeOfMyType t -> typeOfMyType t
negateLike TInt x = -x
negateLike TBool x = not x
Sorry, I meant foreach, not forall ->. (forall ->isRequiredTypeArguments!) Does that resolve the confusion?
I believe “foreach” corresponds to a “Pi-type” or “dependent product” in dependent type theory, and should be possible in Agda, as far as I know. In Haskell it boils down to something like passing Typeable or the singleton for the type in question.
EDIT: I see from your edit that it was a conceptual example of using foreach in a future version of GHC. In the meantime
I’m not sure whether your example was supposed to be literal or conceptual but here’s a literal version that uses a hand-written singleton:
{-# LANGUAGE GHC2024 #-}
import Data.Kind
data SMyType t where
STInt :: SMyType Int
STBool :: SMyType Bool
negateLike :: forall (t :: Type). SMyType t -> t -> t
negateLike STInt x = -x
negateLike STBool x = not x