dependent-type Questions
2
Solved
I try using the syntax for inductive datatypes but it got an error message "mutually inductive types must compile to basic inductive type with dependent elimination".
Below is an example of my att...
Karbala asked 21/1, 2017 at 4:36
1
Solved
The codensity monad on a type constructor f is defined by:
newtype C f a = C { unC ∷ forall r. (a → f r) → f r }
It is well known that C f is a monad for any type constructor f (not necessarily c...
Gumboil asked 19/1, 2023 at 21:13
2
In this article, it is explained that each generic type argument in Scala 3 code is perceived as a dependent type to be conform with the DOT logic:
https://dotty.epfl.ch/docs/internals/higher-kinde...
Bipartite asked 6/1, 2023 at 20:32
2
Solved
I'm trying to compile an Agda file, but I'm having trouble getting it to find the standard library. I've seen the documentation here.
I've used Stack to install it:
> which agda
/home/joey/.lo...
Hervey asked 27/10, 2017 at 21:51
6
Solved
Can someone explain dependent typing to me? I have little experience in Haskell, Cayenne, Epigram, or other functional languages, so the simpler of terms you can use, the more I will appreciate it!...
Orbicular asked 18/2, 2012 at 4:58
2
A simple demo of dependent types in Idris is Vector, whose type depends on its value.
We can use type hints in Python:
from typing import List
def append(a: List[int], b: List[int]) -> List[i...
Aggie asked 8/4, 2017 at 9:10
1
Solved
Wanted to implement type safe matrix multiplication in Haskell.
Defined the following:
{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
module Vector where
data Nat = Succ Nat | Zero
data Vector (...
Featherston asked 17/2, 2022 at 13:58
4
Solved
Assume I want to define types that are similar in structure, but differ in a parameter that could be an integer or could be something else.
Is it possible in Java to define a family of classes para...
Eugene asked 4/8, 2021 at 14:28
2
I would like to define a data type in Haskell which is parametrized by an Int constant along the lines:
data Q (n :: Int) = Q n (Int,Int) -- non-working code
in order to allow me to define function...
Dever asked 15/3, 2021 at 15:52
2
Solved
In a language with dependent types you can have Type-in-Type which simplifies the language and gives it a lot of power. This makes the language logically inconsistent but this might not be a proble...
Lazaro asked 21/5, 2020 at 8:53
2
Solved
Say I have the following constant string:
export default const FOO = 'FOO'
Say I import this in a flow annotated file like so:
import FOO from '../consts/Foo'
I then have a function:
const exa...
Foulk asked 13/2, 2017 at 1:27
4
Solved
I have a custom value type Value labeled by its type ValType:
data ValType
= Text
| Bool
data Value (tag :: ValType) where
T :: Text -> Value 'Text
B :: Bool -> Value 'Bool
and I would ...
Riella asked 20/6, 2020 at 13:48
1
I have a simple case to test the type inference capability of scala:
trait Super1[S] {
final type Out = this.type
final val out: Out = this
}
trait Super2[S] extends Super1[S] {
final typ...
Courtesy asked 19/6, 2020 at 20:18
2
Solved
In languages such as Agda, Idris, or Haskell with type extensions, there is a = type sort of like the following
data a :~: b where
Refl :: a :~: a
a :~: b means that a and b are the same.
Can ...
Untruthful asked 23/3, 2016 at 15:4
1
Assuming that I intend to use the singleton/literal type feature in a scala program, this feature is provided in shapeless library in scala 2.12 (scala 2.13 supports native literal type but let's u...
Tamboura asked 4/6, 2020 at 23:49
1
Solved
How do I correctly type-annotate the function below?
def f(cls: type) -> ???:
return cls()
# Example usage:
assert f(int) == 0
assert f(list) == []
assert f(tuple) == ()
Is there a way to t...
Algometer asked 2/6, 2020 at 13:34
4
Solved
I'm working my way through the chapter 4 of the lean tutorial.
I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other wo...
Stereo asked 30/1, 2017 at 22:11
1
Solved
I am currently implementing derivatives of regular data structures, in Agda,
as presented in the One-Hole Context paper by Conor McBride [5].
In implementing it straight out of the OHC paper, whic...
Champagne asked 15/4, 2020 at 16:21
3
Solved
I would like to make a type that represents lists with a finite number of elements.
Now the naïve way to do this is with strict evaluation:
data FiniteList a
= Nil
| Cons a !(List a)
With thi...
Fetation asked 2/4, 2020 at 1:26
8
Solved
Is there a typed programming language where I can constrain types like the following two examples?
A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.
type Pro...
Behnken asked 4/10, 2013 at 10:26
2
Solved
A simple value hierarchy
Imagine this simple trait Value where every implementing class has a value of some type T.
trait Value {
type T
def value: T
}
We have two different implementing clas...
Reinhold asked 29/11, 2019 at 9:0
1
My issue
I have the following type family that splits arguments off of a function:
type family
SeparateArgs
( a :: Type )
:: ( Type, [Type] )
where
SeparateArgs (a -> b) =
SndCons2 a (Se...
Remand asked 20/11, 2019 at 23:24
1
Consider this Vect type:
{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}
import Data.Kind (Type)
data Nat = Zero | Succ Nat
data Vect :: Nat -> Type -> Type where
Nil :: Ve...
Antifebrile asked 11/11, 2019 at 13:49
3
Consider following definition of a HList:
infixr 5 :>
data HList (types :: [*]) where
HNil :: HList '[]
(:>) :: a -> HList l -> HList (a:l)
And a type family Map to map over typele...
Depressor asked 17/9, 2019 at 11:16
2
Solved
I have been writing Haskell for a while now but wanted to try some experiments with the Idris language, and dependent typing. I have played around a bit, and read the basic doc, however I want to e...
Katmandu asked 20/2, 2016 at 4:57
1 Next >
© 2022 - 2025 — McMap. All rights reserved.